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