[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

On 25/11/2012 20:03, Peter Hancock wrote:
> 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).

I am a bit confused.
Is
  ℕ → ₂
not the space of computable functions from ℕ to ₂?
Are ℕ → ₂, a. and b. three different things, given that the domain is ℕ 
and the image is ₂ ?
Could you highlight the difference?

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

I guess "a relation between Nat and 2 for which it is not absurd that it 
is total" gives the same interpretation for classical sequences as the 
one with "weak values" in the paper "Classical Mathematics for a 
Constructive World".

Is there a question about predicativity here? I just would like to 
translate the infinite pigeonhole principle to Agda as honest as I can.

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