[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

On 27/11/12 21:19, Peter Divianszky wrote:
> Still I have questions:
>
> Can your 'pigeonhole' generalized to functions (ℕ → ¬ ¬ ₂)?

Meaning?

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


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

Very.

> Isn't the latter more "classical"?

What is a classical space?

Best,
Martin