[Agda] Classical Mathematics for a Constructive World

Martin Escardo m.escardo at cs.bham.ac.uk
Tue Nov 27 23:37:36 CET 2012

On 27/11/12 22:21, Peter Divianszky wrote
> There are transformations in both directions; from (¬ ¬ (ℕ → ₂)) to (ℕ →
> ¬ ¬ ₂) we can use the fact that K is a monad.
> These transformations are not the inverses of each-other?
> If yes, do I miss something?

You should really use "K" and not ¬¬ here. Using ¬¬, both spaces have 
precisely one element if you assume function extensionality. If you use 
"K", the left space is much larger than the right space.

>>> Isn't the latter more "classical"?
>> What is a classical space?
> I would use the phrase "classical space" for a space (¬ ¬ A) for some A
> and "classical function space" for a function space (B → ¬ ¬ A). What do
> you think about it?

Spaces of the form ¬¬X have at most one element.


More information about the Agda mailing list