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

[Andrea Vezzosi]

I don't know if it's on the wiki, but _ in Agda's expressions means
"what is uniquely determined by the judgemental equality, using only
the information from this mutual block".

if no such unique solution can be found the _ is going to be left
unspecified and the writer needs to give more details.
So, like in this thread :)


Cheers,
Andrea

On Tue, Oct 14, 2014 at 10:58 PM, Peter Hancock <hancock at fastmail.fm> wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda