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

[Paolo Capriotti]

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