[Agda] (Stronger) double negation of law of excluded middle

[Dmytro Starosud]

Thank you all!
Looks like you gave me enough to read to solve my problem :)

Cheers,
Dima


2014-10-12 17:10 GMT+03:00 Paolo Capriotti <paolo at capriotti.io>:

> On Sun, Oct 12, 2014 at 1:20 PM, Paolo Capriotti <paolo at capriotti.io>
> wrote:
> >
> > That raises a further question: is the statement
> >
> >     not not ((A : Prop) -> A + not A)
> >
> > provable (where Prop = Σ (A : Set) . isProp(A))?
>
> The answer should be no again. I think it suffices to look at the
> copresheaf category Set^ω. There, if I'm not mistaken, the type
> corresponding to "propositional" LEM is not just uninhabited, but
> globally 0.  Therefore its double negation is 0 as well.
>
> Paolo
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141012/194673d7/attachment-0001.html