[Agda] Classical Mathematics for a Constructive World
Peter Divianszky
divipp at gmail.com
Tue Nov 27 18:27:59 CET 2012
> 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
More information about the Agda
mailing list