[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

>> I can't find a transformation from (ℕ → ¬ ¬ ₂) to (¬ ¬ (ℕ → ₂)).
>
> The first person to find such a function was Spector in the late 1950's
> or early 1960's. The recursion scheme used to define it is called
> (Spector) bar recursion.
>
> Other recursion schemes were given much more recently by
> Berardi-Bezem-Coquand (end of last millennium), Berger (early this
> millennium), Escardo-Oliva (some years ago).
>
> The Agda pigeon program can run with any of the three in the last
> paragraph, and there is a file in which you can choose which one you
> want to use. The default choice is selfish.
>
> A tutorial paper about the EO functional is here:
> http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/

Sorry, I forgot these definitions.
Thanks!

 >> Can your 'pigeonhole' generalized to functions (ℕ → ¬ ¬ ₂)?
 >
 > Meaning?

Now that I can transform any sequence from (ℕ → ¬ ¬ ₂) to (¬ ¬ (ℕ → ₂)),
I transform the sequence and apply 'pigeonhole' in the K monad, which 
gives the meaning now.

>> Are the spaces (¬ ¬ (ℕ → ₂)) and (ℕ → ¬ ¬ ₂) different?
>
> Very.

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?

>> 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?

Sorry for my constant questions and thanks a lot,

Peter