[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.
Best,
Martin
More information about the Agda
mailing list