The principles you seek are there, but they are simply true, unless you work with a hampered foundation or you mix things up and phrase them badly. Allow me to give a short overview. I trust you will be able to pick and choose from it what you need.
I shall work in set theory, and comment on type theory at the end. Write $\Omega$ for the set of all propositions (in type theory usually written as $\mathsf{Prop}$), so the predicates on a set $A$ are the same thing as maps $A \to \Omega$. We also identify the powerset $P(A)$ with $A \to \Omega$. Thus for $S \in P(A)$ the notation $x \in S$ is just shorthand for $S x$.
The singleton $\{x\}$ corresponding to a given $x \in A$ is the map $\{x\} : A \to \Omega$ defined by $\{x\} y = (x = y)$, which is just the transposition of identity ${=} : A \times A \to \Omega$.
To deal with partial maps we define for each set $A$ its set of partial elements $\tilde{A}$ by
$$\tilde{A} = \{p : A \to \Omega \mid
\forall x, y \in A .\, p x \land p y \Rightarrow x = y
\}.$$
We think of $\emptyset$ as “undefined” and a singleton $\{x\}$ as “defined” (and there are no other elements in $\tilde{A}$).
Do not confuse $\tilde{A}$ with $1 + A$, or $\mathsf{option}(A)$, for $\tilde{A} \cong 1 + A$ implies excluded middle!
A partial map from $X$ to $Y$ can be thought of as a map $X \to \tilde{Y}$.
To deal with multivalued maps, define for each set $A$ the set of multivalues $P_*(A)$ by
$$P_*(A) = \{ p : A \to \Omega \mid \exists x \in A .\, p x\}.$$
A multivalued map from $X$ to $Y$ can be thought of as a map $X \to P_*(Y)$.
Let us also define the somewhat silly looking
$$
S(A) = \tilde{A} \cap P_*(A) =
\{p : A \to \Omega \mid
\exists x \in A . p x \land \forall y \in A . p y \Rightarrow x = y \}.
$$
It is the set of all singletons of $A$. The inverse $\iota : S(A) \to A$ of the singleton map $\{{-}\} : A \to S(A)$ is known as the definite description operator. Its existence is equivalent to unique choice.
A relation $\phi : A \times B \to \Omega$ is:
- single-valued when $\forall x \in A . \forall y, z \in B . \phi(x,y) \land \phi(x,z) \Rightarrow y = z$,
- total when $\forall x \in A . \exists y \in B . \phi (x, y)$,
- functional when it is total and single-valued.
We may now write down three principles which are simply true:
- Single-valued relations $A \times B \to \Omega$ are in bijective correspondence with maps $A \to \tilde{B}$.
- Total relations $A \times B \to \Omega$ are in bijective correspondence with maps $A \to P_*(B)$.
- Functional relations $A \times B \to \Omega$ are in bijective correspondence with maps $A \to S(B)$.
In all three cases the proof goes as follows: a relation $\phi : A \times B \to \Omega$ may be transposed to a map $\overline{\phi} : A \to (B \to \Omega)$ defined by $\overline{\phi} x = \lambda y . \phi(x,y)$, which is precisely the one we're looking for in each of the three cases.
The above three principles are equivalent to the logical statements, for $\phi : A \times B \to \Omega$:
A single-valued relation is the graph of a partial map:
\begin{multline*}
(\forall x \in A . \forall y, z \in B . \phi (x, y) \land \phi x z \Rightarrow y = z)
\Rightarrow \\
\exists f : A \to \tilde{B} . \forall x \in A . \forall y \in B .
(p x y \Leftrightarrow y \in f(x)).
\end{multline*}
A total relation is the graph of a multivalued map:
\begin{multline*}
(\forall x \in A . \exists y \in B . \phi (x, y))
\Rightarrow
\exists f : A \to P_*(B) . \forall x \in A . \forall y \in B .
(p x y \Leftrightarrow y \in f(x)).
\end{multline*}
A functional relation is the graph of a singleton-valued map:
\begin{multline*}
(\forall x \in A . \exists! y \in B . \phi (x, y))
\Rightarrow
\exists f : A \to S(B) . \forall x \in A . \forall y \in B .
(p x y \Leftrightarrow y \in f(x)).
\end{multline*}
I will leave these as exercises – they are all true.
If unique choice holds then the definite description operator $\iota$ can be used to replace $S(B)$ with $B$:
\begin{multline*}
(\forall x \in A . \exists! y \in B . \phi (x, y))
\Rightarrow
\exists f : A \to B . \forall x \in A . \forall y \in B .
(p x y \Leftrightarrow y = f(x)).
\end{multline*}
This form is the usual statement of unique choice. It implies the existence of $\iota$.
Observe that $A \mapsto \tilde{A}$, $A \mapsto P_*(A)$ and $A \mapsto S(A)$ are all monads (and the last one is trivial when unique choice holds). The monad structure is induced by the covariant powerset monad.
By altering the monads we obtain variations.
For example, if we replace $\Omega$ with decidable truth values $\mathsf{Bool} = \{p \in \Omega \mid p \lor \neg p\}$, then $P(A)$ is the set of decidable subsets of $A$ and $\tilde{A} \cong 1 + A$ (also known as $\mathsf{option}(A)$ in type theory).
Another example is $\Omega$ is replaced with semidecidable truth values
$$\Sigma = \{p \in \Omega \mid \exists f : \mathbb{N} \to \mathsf{Bool} . (p \Leftrightarrow \exists n . f n)\}.$$
In type theory this one is known as the delay monad.
When we switch from set theory to type theory we may replace $\Omega$ with $\mathsf{Prop}$ (or even $\mathsf{Type}$). The principles will still hold, and the existence of $\iota$ will hinge on the usual nuances about $\Sigma$ vs. $\exists$ and elimination from propositions into types.
natcome from? $\endgroup$