nLab principle of unique choice

Principle of Unique Choice




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

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

ΓAtypeΓ,x:ABtypeΓ,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 \; \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)}


Last revised on December 14, 2022 at 20:26:58. See the history of this page for a list of all contributions to it.