[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

> 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