[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

On 19/11/2012 14:47, Martin Escardo wrote:
> The following Agda code is related:
>
> http://www.cs.bham.ac.uk/~mhe/pigeon/
>
> It uses the generalized double negation monad X |-> (X->R)->R to code a
> classical proof in Agda (without postulating excluded middle).
>
> Martin

Thanks.
I've read the code, it is clearly written.

Is it true, that if one would use the double-negation monad, the 
computable finite pigeonhole principle could not be derived from the 
infinite one?

Peter


> On 19/11/12 12:44, Peter Divianszky wrote:
>> Excuse me that this time I flood the mailing list with questions.
>>
>> I have read "Classical Mathematics for a Constructive World", by Russell
>> O’Connor, http://arxiv.org/pdf/1008.1213
>>
>> Does someone implemented part of the paper in Agda?
>>
>> Thanks,
>> Peter
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>