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

[Paolo Capriotti]

On Tue, Oct 14, 2014 at 9:58 PM, Peter Hancock <hancock at fastmail.fm> wrote:
> This is a sidetrack.  I'm puzzled about what "_" means in Agda, and often
> encounter this puzzle. (I've no (known) problem with "_" in Haskell, which
> AFAIK only
> occurs in argument position and means "I need no name for this argument",
> and
> is a very worthwhile flag that the name would be unused.)
>
> The way I read the above, "_" means "the obvious thing", which in this case
> is
> surely the identity. So PROP means "inhabited type".  And isProp A is a
> roundabout
> way of writing A.

I thought "_" was just (informally) used as a placeholder there. I
don't think this would be valid Agda.

For me, `isProp` is defined as usual in HoTT, i.e.:

    isProp : Set -> Set
    isProp X = (x y : X) -> x = y

where _=_ is propositional equality.

>
> So not not ((A : Set) -> isProp A -> A + not A) should be trivial. It is the
> left
> injection, smashed down with not not.

No, `isProp A` is not the same as `A`.

>
> I completely see that  ((A : Set) -> not not ( A + not A)) (which is true --
> no ??)
> is something different from not not ( (A : Set) -> A + not A ) (which one
> can possibly
> find a counterexample for using Kripke models for 2nd order logic, or
> whatever is the
> latest technology.)

Yes, that's the gist of the discussion. I added `isProp` into the mix
just because one can show that `not not ((A : Set) -> A + not A)` is
not provable simply by observing that it contradicts univalence, but
you really need to bring on Kripke models for the "squashed" version
with `isProp`.

Paolo