[Agda] excluded-middle

Martín Hötzel Escardó m.escardo at cs.bham.ac.uk
Tue Jun 21 12:43:02 CEST 2016



On 21/06/16 08:08, Nils Anders Danielsson wrote:
> On 2016-06-20 22:57, Martin Escardo wrote:
>> [...] but the intuitionistically valid principle that not-not(every
>> type has an inhabitant or not).
>
> Or rather "for every type, not not (this type has an inhabitant or
> not)".

All that glitters is not gold. :-)

Martin


More information about the Agda mailing list