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, the type-theoretic principle of unique choice states that the dependent product type of a family of contractible types is pointed.

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isContr}(B(x))}{\Gamma\vdash \mathrm{uniquechoice}(\lambda x.p(x)):\prod_{x:A} B(x)}$$

The principle of unique choice is not equivalent to weak function extensionality. Weak function extensionality states that the dependent product type of a family of contractible types is contractible

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isContr}(B(x))}{\Gamma\vdash \mathrm{weakfunext}(\lambda x.p(x)):\mathrm{isContr}\left(\prod_{x:A} B(x)\right)}$$

However, this is not the same principle of unique choice as in set theory. The set-theoretic principle of unique choice in states that every proposition-valued binary type family $x:A, y:B \vdash C(x, y)$ which is functional and total determines a necessarily unique function, and is only true for propositional-valued binary type families in dependent type theory for which the second index type $B$ is a set. Making the set-theoretic principle of unique choice hold for all types is tantamount to saying that all types are sets; thus the set-theoretic principle of unique choice makes the type theory into a set-level type theory.

Related concepts

• anafunction

References

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