[Agda] Classical Mathematics for a Constructive World

Peter Divianszky divipp at gmail.com
Sat Nov 24 17:25:38 CET 2012

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

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?


> 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

More information about the Agda mailing list