[Agda] Re: Classical Mathematics for a Constructive World

[Jan Burse]

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?

Bye