[Agda] consistency

[Patricia Peratto]

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.

-- 
/NAD