nLab principle of unique choice

Principle of Unique Choice




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Principle of Unique Choice


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)SetAdj(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.

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isContr(B(x))Γuniquechoice(λx.p(x)): x:AB(x)\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

ΓAtypeΓ,x:ABtypeΓ,x:Ap(x):isContr(B(x))Γweakfunext(λx.p(x)):isContr( x:AB(x))\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:BC(x,y)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 BB 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.


Last revised on July 25, 2023 at 18:18:43. See the history of this page for a list of all contributions to it.