[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

Third question. Have you answered it yourself?

You seem to want to define classical sequence. Then, well, maybe ¬¬(the 
space of sequences), and its K-generalizations (or J-generalizations, if 
you look at the link of the previous message), may be one possible kind 
of answer. Peter Hancock gave another possible answer. And I think 
similar to Russell's paper.

Martin


On 27/11/12 17:27, Peter Divianszky wrote:
>
>> I have a question.
>> In module InfinitePigeon you have defintions
>>
>> ------------------------------------------
>> Pigeonhole : {R : Ω} → ₂ℕ → Ω
>> Pigeonhole {R} α =
>>     ∃ \(b : ₂) → ∃ \(g : ℕ → ℕ) →
>>     ∀(i : ℕ) → g i < g(i + 1) ∧ K {R} (α(g i) ≡ b)
>>
>>
>> pigeonhole : {R : Ω} →
>> ----------
>>      ∀(α : ₂ℕ) → K(Pigeonhole α)
>> pigeonhole R α = ...
>> ------------------------------------------
>>
>> Could we replace 'Pigeonhole' and 'pigeonhole' with these:
>>
>> ------------------------------------------
>> Pigeonhole : {R : Ω} → K {R} ₂ℕ → Ω
>> Pigeonhole {R} α = ...
>>
>> pigeonhole : {R : Ω} →
>> ----------
>>      ∀(α : K {R} ₂ℕ) → K(Pigeonhole α)
>> pigeonhole R α = ...
>> ------------------------------------------
>
> I think the answer is yes, because 'K {R}' is a monad.
> And we don't have to modify your definitions to use 'pigeonhole' with
> sequences 'K {R} ₂ℕ' (these could be called classical sequences).
>
> In this case I have got positive answers to my questions.
>
> Thank you very much!
>
> Peter
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe