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

[Dmytro Starosud]

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)

Probably in Agda it is still possible to prove this?

Thanks,
Dmytro


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

> On Sun, Oct 12, 2014 at 8:24 AM, Dmytro Starosud <d.starosud at gmail.com>
> wrote:
> > Which models do you mean?
> > Please share few keywords to google, or links.
>
> There are models in which there exists a (small) type `X` such that `X
> + not X` is *not* inhabited (e.g. any non-boolean Grothendieck topos).
> In such a model, the type `not ((A : Set) -> A + not A)` is inhabited.
> It follows that the type corresponding to the statement you want to
> prove is not.
>
> Paolo
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141012/6b7c8c4e/attachment.html