[Agda] Running a classical proof with choice in Agda

[Martin Escardo]

On 09/05/11 10:56, Thorsten Altenkirch wrote:
> Why has pigeonhole a hidden parameter R which is not referenced in the rest of the type?

Ah! Because I want to write KA and JA assuming an implicit R, where 
KA=((A->R)->R). I disambiguate the R in the proof of the theorems, when 
possible, rather than in their formulation, hoping that readers will 
know that I always mean R (as we do in the publications).

> I guess the definition of pigeonhole unifies R with the first parameter to Pigeonhole but this should be expressed in the type.

I thought omitting R would avoid much clutter, as all occurrences of K 
are meant to use that R (and it does), probably making things clearer 
overall.

> I suspect it may be better to turn R (i.e. the type of responses for the continuations) into a module parameter instead of threading it through the definitions.

Yes, this is probably better. Perhaps in a future version I should try 
that.

> A more general question: Implementing Markov's principle in a naive way destroys termination for open terms. Is this avoided here? I suspect not...

I will give a reply as a reply to Thierry's reply to you.

Best wishes,
Martin