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

[Paolo Capriotti]

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