[Agda] Classical Mathematics for a Constructive World

Martin Escardo m.escardo at cs.bham.ac.uk
Sun Nov 25 19:35:31 CET 2012

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:

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


More information about the Agda mailing list