[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

On 19/11/2012 13:56, Nils Anders Danielsson wrote:
> On 2012-11-19 13:44, Peter Divianszky wrote:
>> 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?
>
> The paper mentions the double-negation monad, which is available in the
> standard library:
>
> http://www.cse.chalmers.se/~nad/listings/lib-0.6/Relation.Nullary.Negation.html
>
> http://www.cse.chalmers.se/~nad/listings/lib-0.6/Relation.Nullary.Universe.html

Thanks.

I noticed that "Classical Mathematics for a Constructive World" is not 
published.
Also "A computer-checked proof of the four colour theorem." (2005) a 
work in Coq by Georges Gonthier is not published.
By any chance, do you know why?
I'm going to give a presentation for mathematicians and they may ask the 
same.

Peter