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

[Peter Hancock]

On 14/10/2014 21:30, Paolo Capriotti wrote:
> 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

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.

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

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.)

I'm just asking what "_" means in Agda. It's not obvious to me. Can someone point me
into the Wiki?

Peter