[Agda] Classical Mathematics for a Constructive World

[Nils Anders Danielsson]

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

-- 
/NAD