[Agda] consistency

[James Wood]

Hi Patricia,

Plain Agda minus K is meant to be consistent with homotopy type theory,
in which it is false that constructors are injective (due to higher
inductive types). Thus there is not much motivation to support
injectivity of (most) constructors other than the practical benefit of
being able to match a proof of 0 ≡ 1 with the absurd pattern.

Perhaps you are looking for a size-limited system that nonetheless
supports absurd patterns? As far as I'm aware, all practical proof
assistants assume countably infinitely many universes.

Regards,
James

On 07/02/2020 18:09, Patricia Peratto wrote:
> By example, to prove 0<>1 one uses universes.
> And uses the Bottom Set and the True set together
> with substitutivity.
> 
> If you put as an axiom that different constructors
> give different elements in the same set, you
> don't need to use Bottom.
> 
> 
> Regards,
> Patricia.
> 
> ----- Mensaje original -----
> De: "Nils Anders Danielsson" <nad at cse.gu.se>
> Para: "Patricia Peratto" <psperatto at vera.com.uy>
> Enviados: Viernes, 7 de Febrero 2020 7:23:19
> Asunto: Re: [Agda] consistency
> 
> On 2020-02-02 01:19, Patricia Peratto wrote:
>> Can not be defined as an axiom that different
>> constructors create different terms?
>>
>> To prove 0<>1 without using bottom.
>> To be consistent.
> 
> I don't understand what you mean. If you can rephrase your question and
> resend it to the list, then perhaps you will get an answer.
>