[Agda] Classical Mathematics for a Constructive World

Nils Anders Danielsson nad at chalmers.se
Mon Nov 19 13:56:33 CET 2012

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:



More information about the Agda mailing list