Return to Answer

Question 1] Morphisms $\lambda:X\times Y\to\Omega$ correspond to subobjects $L\subseteq X\times Y$. The conditions ed says that the projection $\pi_0:L\to X$ is a (regular) epimorphism, and uv says that $\pi_0$ is a monomorphism. Therefore $\pi_0$ is an isomorphism, and $l = \pi_1\circ \pi_0^{-1}:X\to Y$ is the corresponding morphism. In the other direction, for each $l:X\to Y$ there is a graph ${\rm gr}(l)\subseteq X\times Y$. The projection $\pi_0:{\rm gr}(l) \to X$ is an isomorphism, and hence satisfies ed and uv. This sets up a bijection between functional relations and morphisms in a topos.

Subquestion] these are provably equivalent in first order constructive logic.

Question 2] It should be $f_*\Omega_{\mathcal F}$, because $f_* :\mathcal F\to\mathcal E$. Now we are dealing with naturally equivalent locales, $\mathcal F(X\times Y,f_*\Omega)\simeq \mathcal E(f^*X\times f^*Y,\Omega)$. Hence the morphisms satisfying ed and uv coincide.

Question 1] Morphisms $\lambda:X\times Y\to\Omega$ correspond to subobjects $L\subseteq X\times Y$. The conditions ed says that the projection $\pi_0:L\to X$ is a (regular) epimorphism, and uv says that $\pi_0$ is a monomorphism. Therefore $\pi_0$ is an isomorphism, and $l = \pi_1\circ \pi_0^{-1}:X\to Y$ is the corresponding morphism. In the other direction, for each $l:X\to Y$ there is a graph ${\rm gr}(l)\subseteq X\times Y$. The projection $\pi_0:{\rm gr}(l) \to X$ is an isomorphism, and hence satisfies ed and uv. This sets up a bijection between functional relations and morphisms in a topos.

Subquestion] these are provably equivalent in first order constructive logic.

Question 2] It should be $f_*\Omega_{\mathcal F}$, because $f_* :\mathcal F\to\mathcal E$. Now we are dealing with naturally equivalent locales, $\mathcal E(X\times Y,f_*\Omega)\simeq \mathcal F(f^*X\times f^*Y,\Omega)$. Hence the morphisms satisfying ed and uv coincide.

Question 1] Morphisms $\lambda:X\times Y\to\Omega$ correspond to subobjects $L\subseteq X\times Y$. The conditions ed says that the projection $\pi_0:L\to X$ is a (regular) epimorphism, and uv says that $\pi_0$ is a monomorphism. Therefore $\pi_0$ is an isomorphism, and $l = \pi_1\circ \pi_0^{-1}:X\to Y$ is the corresponding morphism. In the other direction, for each $l:X\to Y$ there is a graph ${\rm gr}(l)\subseteq X\times Y$. The projection $\pi_0:{\rm gr}(l) \to X$ is an isomorphism, and hence satisfies ed and uv. This sets up a bijection between functional relations and morphisms in a topos.

Subquestion] these are provably equivalent in first order constructive logic.

Question 2] It should be $f_*\Omega_{\mathcal F}$, because $f_* :\mathcal F\to\mathcal E$. Now we are dealing with naturally equivalent locales, $\mathcal E(X\times Y,f_*\Omega)\simeq \mathcal E(f^*X\times f^*Y,\Omega)$. Hence the morphisms satisfying ed and uv coincide.

Question 1] Morphisms $\lambda:X\times Y\to\Omega$ correspond to subobjects $L\subseteq X\times Y$. The conditions ed says that the projection $\pi_0:L\to X$ is a (regular) epimorphism, and uv says that $\pi_0$ is a monomorphism. Therefore $\pi_0$ is an isomorphism, and $l = \pi_1\circ \pi_0^{-1}:X\to Y$ is the corresponding morphism. In the other direction, for each $l:X\to Y$ there is a graph ${\rm gr}(l)\subseteq X\times Y$. The projection $\pi_0:{\rm gr}(l) \to X$ is an isomorphism, and hence satisfies ed and uv. This sets up a bijection between functional relations and morphisms in a topos.

Subquestion] these are provably equivalent in first order constructive logic.

Question 2] It should be $f_*\Omega_{\mathcal F}$, because $f_* :\mathcal F\to\mathcal E$. Now we are dealing with naturally equivalent locales, $\mathcal F(X\times Y,f_*\Omega)\simeq \mathcal E(f^*X\times f^*Y,\Omega)$. Hence the morphisms satisfying ed and uv coincide.

Question 1] Morphisms $\lambda:X\times Y\to\Omega$ correspond to subobjects $L\subseteq X\times Y$. The conditions ed says that the projection $\pi_0:L\to X$ is a (regular) epimorphism, and uv says that $\pi_0$ is a monomorphism. Therefore $\pi_0$ is an isomorphism, and $l = \pi_1\circ \pi_0^{-1}:X\to Y$ is the corresponding morphism. In the other direction, for each $l:X\to Y$ there is a graph ${\rm gr}(l)\subseteq X\times Y$. The projection $\pi_0:{\rm gr}(l) \to X$ is an isomorphism, and hence satisfies ed and uv. This sets up a bijection between functional relations and morphisms in a topos.

Subquestion] these are provably equivalent in first order constructive logic.

Question 2] this depends on whether $\bigvee$ commutes with this bijection, which I am unsure of.

Question 1] Morphisms $\lambda:X\times Y\to\Omega$ correspond to subobjects $L\subseteq X\times Y$. The conditions ed says that the projection $\pi_0:L\to X$ is a (regular) epimorphism, and uv says that $\pi_0$ is a monomorphism. Therefore $\pi_0$ is an isomorphism, and $l = \pi_1\circ \pi_0^{-1}:X\to Y$ is the corresponding morphism. In the other direction, for each $l:X\to Y$ there is a graph ${\rm gr}(l)\subseteq X\times Y$. The projection $\pi_0:{\rm gr}(l) \to X$ is an isomorphism, and hence satisfies ed and uv. This sets up a bijection between functional relations and morphisms in a topos.

Subquestion] these are provably equivalent in first order constructive logic.

Question 2] It should be $f_*\Omega_{\mathcal F}$, because $f_* :\mathcal F\to\mathcal E$. Now we are dealing with naturally equivalent locales, $\mathcal E(X\times Y,f_*\Omega)\simeq \mathcal E(f^*X\times f^*Y,\Omega)$. Hence the morphisms satisfying ed and uv coincide.