Unique choice

The principle of unique choice (aka function comprehension) is the idea that total functional relations and functions correspond precisely.

In higher-order logic

In HOL this principle can be written as follows: for any types A and B,

\forall R : A \to B \to \textsf{Prop}.\  (\forall a : A.\, \exists! b : B.\, R(a, b)) \to (\exists f : A \to B.\, \forall a : A.\, R(a, f(a))

The quantifier \exists! is interpreted as "there exists a unique element". Thus, if we have for every a : A a unique choice of b : B such that R(a, b), then this choice can be bootstrapped into a function f : A \to B.

References

• nLab page

• The principle of unique choice is "familiar from topos theory." Any leads on that?