nLab principle of unique choice

Idea

The principle of unique choice, also known as function comprehension, is the principle that every total functional relation determines a (necessarily unique) function.

This is true in classical logic and most forms of intuitionistic logic (for example the internal language of any topos), but fails in weaker systems such as the internal language of a tripos, or one of the internal languages of a quasitopos.

2-Categorical Formulation

A total, functional relation is precisely an adjunction in the bicategory of relations Rel. So the principle of unique choice can be seen as a functor $Adj(Rel) \to Set$, in fact, an equivalence of categories. For this reason, bicategories modeling relations such as cartesian bicategories or allegories can be used to model functions as well by using the adjoint pairs of relations.

However, note that a generalization from Rel to the bicategory Prof of categories and profunctors is not possible: in general an adjoint pair of profunctors determines only a semifunctor, which can be improved to a functor if the codomain category is Cauchy complete. For this reason, sometimes people use algebraic structures modeling profunctors such as proarrow equipments and virtual double categories that include notions of functor in addition to profunctor.

In dependent type theory

In dependent type theory, unique choice can be formulated as for any $A : \text{Type}$, $B : A \to \text{Type}$ and $R : (a : A) \to B(a) \to \text{Type}$ that

$$((a : A) \to \exists ! (b : B(a)) , R(a)(b)) \to \exists ! (f : (a : A) \to B(a)) , (a : A) \to R(a)(f(a))$$

Whether unique choice is provable or not depends mostly on what notion of proposition is used. It is not provable using the primitive notion of proposition in OTT or Rocq.

However, if we use the notion of mere proposition in homotopy type theory and interpret unique existence as $\exists ! (x : X) , P(x) \coloneqq \text{is-contr} (\sum_{x : X} P(x))$ (see uniqueness quantifier.), then this is provable in MLTT in the presence of function extensionality (see ME2019.)

Related concepts

• anafunction

References

• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Project, Institute for Advanced Study, 2013. (web, pdf)

• Introduction to Univalent Foundations of Mathematics with Agda, Martín Hötzel Escardó, 2019. (web)