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

[Paolo Capriotti]

On Tue, Oct 14, 2014 at 9:28 PM, Dmytro Starosud <d.starosud at gmail.com> wrote:
> Btw, I was trying to look into this, but there is something missing with it:
>
> isProp : Set → Set
> isProp = _
>
> PROP = ∃ λ A → isProp A
>
> prop : ¬ ¬ ((A : PROP) → A ⊎ ¬ A)
> prop = _
>
> Agda doesn't want type check type of little prop
> _⊎_ expects types as an arguments and negation expects type as an argument
> but A is of type PROP and thus is not type, but term.
>
> Could you clarify what you meant to write? (unfortunately I failed to
> recover original meaning)

I was a bit sloppy with the notation. I meant:

    not not ((A : Set) -> isProp A -> A + not A)

Paolo