[Agda] Re: Classical Mathematics for a Constructive World

Jan Burse janburse at fastmail.fm
Mon Nov 19 16:23:16 CET 2012

Martin Escardo schrieb:
> 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

Do you think, since it is not postulated, it is not
derivable via some of the translations given in the paper?


More information about the Agda mailing list