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

[Paolo Capriotti]

On Sun, Oct 12, 2014 at 12:05 PM, Dmytro Starosud <d.starosud at gmail.com> wrote:
> Looks really interesting; I will definitely look into it.
>
> But currently it is out of scope of my question. All I need is to
> investigate this inside Agda.
> And In Agda I can prove that you cannot give me such `X` for which `X + not
> X` is *not* inhabited (see `not-In-Agda` below):
>
> ¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)
> ¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))
>
> not-In-Agda : ¬ (Σ Set λ X → ¬ (X ⊎ ¬ X))
> not-In-Agda (X , p) = ¬¬lem′ X p
>
> So, it's not the case in [at least 'standard'] Agda.
> (Or probably I am missing the key essence of your message :-D)

Well, I wrote that `X` is such that `X + not X` is not inhabited, but
that doesn't mean that `not (X + not X)` is inhabited, so there's no
contradiction here.

Nevertheless, I realised that what I wrote is incorrect. The negation
of LEM is not (globally) true in the topos I was thinking about, so
the statement you want to prove actually holds there. Sorry about
that.

It is still true that the statement is unprovable, but the argument
needs to be a bit subtler. For example, Corollary 3.2.7 in the HoTT
book (http://homotopytypetheory.org/book/) shows that any model of
type theory compatible with univalence falsifies the statement.

That raises a further question: is the statement

    not not ((A : Prop) -> A + not A)

provable (where Prop = Σ (A : Set) . isProp(A))?

Paolo