[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

On 25/11/12 13:06, Peter Divianszky wrote:
> In the statement of the main theorem you use
>
> ₂ℕ : Set
> ₂ℕ = ℕ → ₂
>
> which are the computable sequences of Booleans and
> not all the classical sequences as I understand.
> Should not the theorem be proved for classical sequences, provided that
> it is a translation of a classical theorem?

One possible answer is this:

     http://math.fau.edu/richman/HTML/CONSTRUC.HTM
     Fred Richman

     "Every theorem in constructive mathematics can be understood as
     referring to the conventional universe of mathematical discourse,
     and the proofs are acceptable within that universe. We do not
     limit ourselves to a restricted class of "constructive objects""

Martin