[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

Still I have questions:

Can your 'pigeonhole' generalized to functions (ℕ → ¬ ¬ ₂) ?

I can't find a transformation from (ℕ → ¬ ¬ ₂) to (¬ ¬ (ℕ → ₂)).

Are the spaces (¬ ¬ (ℕ → ₂)) and (ℕ → ¬ ¬ ₂) different?

Isn't the latter more "classical"?

Thanks,

Peter


On 27/11/2012 18: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
>