[Agda] Re: Classical Mathematics for a Constructive World

[Jan Burse]

Jan Burse schrieb:
> I get:
>
>     P(x,z) -> forall y (C(x,y) -> Q(y,z))
>
> Question is now whether this implies:
>
>     P(x,z)&R(z) -> forall y(C(x,y) -> Q(y,z)&R(z))
>
> I guess the answer is affirmative already in
> minimal logic. But I might be also wrong here.


Ramana Kumar just wrote me:
 > The * is not just conjunction, it is separating
 > conjunction. Maybe you know that already, but just
 > to make sure, the semantics of P * R is (P * R)(x,h)
 > = exists h1. exists h2. h = h1 + h2 & P(x,h1) & R(x,h2)
 > where + is disjoint union. The choice issue is that the
 > h2 for R on the Q * R side doesn't have to be the same.

In as far is this related to a choice principle? A
choice principle says whether a choice always exists
or not. It is not so much concerned with the stability
of a choice, that might or might not exists.

What is a typical counter example?