[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

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.

Best,
Martin