[Agda] Classical Mathematics for a Constructive World

[Peter Hancock]

Some thoughts prompted by your question.

> I have another question.
> 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?

1. If we wanted to prove something specifically about computable sequences, then we could either prove it about
    a. sequences for which there is a turing machine computing extensionally the same function.
    b. sequences for which it is not absurd that there exists...(ditto).

2. What is a classical sequence?  Conceivably, it is a relation between Nat and 2 for which it is
    not absurd that it is total.  Maybe this gets us into problems with predicativity; because
    quantifying over relations is (from a predicative p.o.v) like quantifying over proper classes.
    As far as I know, predicativity makes sense classically.

So, not a yes/no answer.  What do you think?

Peter