# 2.15 Universal properties

###### Theorem 2.15.2.

(2.15.1) is an equivalence.

###### Proof.

Now given $f:X\to A\times B$, the round-trip composite yields the function

 ${\lambda}x.\,(\mathsf{pr}_{1}(f(x)),\mathsf{pr}_{2}(f(x))).$ (2.15.3)

By Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1), for any $x:X$ we have $(\mathsf{pr}_{1}(f(x)),\mathsf{pr}_{2}(f(x)))=f(x)$. Thus, by function extensionality, the function (2.15.3) is equal to $f$.

On the other hand, given $(g,h)$, the round-trip composite yields the pair $({\lambda}x.\,g(x),{\lambda}x.\,h(x))$. By the uniqueness principle for functions, this is (judgmentally) equal to $(g,h)$. ∎

In fact, we also have a dependently typed version of this universal property. Suppose given a type $X$ and type families $A,B:X\to\mathcal{U}$. Then we have a function

 $\Bigl{(}\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}(A(x)\times B(x))% \Bigr{)}\to\Bigl{(}\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x)% \Bigr{)}\times\Bigl{(}\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_% {(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}B(x)\Bigr{)}$ (2.15.4)

defined as before by $f\mapsto(\mathsf{pr}_{1}\circ f,\mathsf{pr}_{2}\circ f)$.

###### Theorem 2.15.5.

(2.15.4) is an equivalence.

###### Proof.

Just as $\Sigma$-types are a generalization  of cartesian products, they satisfy a generalized version of this universal property. Jumping right to the dependently typed version, suppose we have a type $X$ and type families $A:X\to\mathcal{U}$ and $P:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:% X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x)\to\mathcal{U}$. Then we have a function

 $\Bigl{(}\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}\sum_{(a:A(x))}\,% P(x,a)\Bigr{)}\to\Bigl{(}\mathchoice{\sum_{(g:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x))}\,}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{% \prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x% :X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{% \prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(% x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}}}{\sum_{(g:\mathchoice{\prod_{x:X}% \,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod% _{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}% }{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_% {(x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{% {\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:X% }\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{% \prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{% {\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:X% }\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{% \prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{% {\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}}\mathchoice{\prod_{(x:X)}\,}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}P(x,g(x))\Bigr{)}.$ (2.15.6)

Note that if we have $P(x,a):\!\!\equiv B(x)$ for some $B:X\to\mathcal{U}$, then (2.15.6) reduces to (2.15.4).

###### Theorem 2.15.7.

(2.15.6) is an equivalence.

###### Proof.

As before, we define a quasi-inverse to send $(g,h)$ to the function ${\lambda}x.\,(g(x),h(x))$. Now given $f:\mathchoice{\prod_{(x:X)}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(% x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}\mathchoice{\sum_{(a:A(x))% }\,}{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}% }{\sum_{(a:A(x))}}}{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{\sum_{(a:A(x))}}{% \sum_{(a:A(x))}}{\sum_{(a:A(x))}}}{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{% \sum_{(a:A(x))}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}}P(x,a)$, the round-trip composite yields the function

 ${\lambda}x.\,(\mathsf{pr}_{1}(f(x)),\mathsf{pr}_{2}(f(x))).$ (2.15.8)

Now for any $x:X$, by Corollary 2.7.3 (http://planetmath.org/27sigmatypes#Thmprecor1) (the uniqueness principle for $\Sigma$-types) we have

 $(\mathsf{pr}_{1}(f(x)),\mathsf{pr}_{2}(f(x)))=f(x).$

Thus, by function extensionality, (2.15.8) is equal to $f$. On the other hand, given $(g,h)$, the round-trip composite yields $({\lambda}x.\,g(x),{\lambda}x.\,h(x))$, which is judgmentally equal to $(g,h)$ as before. ∎

This is noteworthy because the propositions-as-types interpretation   of (2.15.6) is “the axiom of choice  ”. If we read $\Sigma$ as “there exists” and $\Pi$ (sometimes) as “for all”, we can pronounce:

• $\mathchoice{\prod_{(x:X)}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:% X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}\mathchoice{\sum_{(a:A(x))% }\,}{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}% }{\sum_{(a:A(x))}}}{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{\sum_{(a:A(x))}}{% \sum_{(a:A(x))}}{\sum_{(a:A(x))}}}{\mathchoice{{\textstyle\sum_{(a:A(x))}}}{% \sum_{(a:A(x))}}{\sum_{(a:A(x))}}{\sum_{(a:A(x))}}}P(x,a)$ as “for all $x:X$ there exists an $a:A(x)$ such that $P(x,a)$”, and

• $\mathchoice{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{% (x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}% \,}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:X% }\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{% \prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{% {\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{x:X% }\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{% \prod_{(x:X)}}{\prod_{(x:X)}}}A(x))}}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(% x:X)}}{\prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{% {\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}{\sum_{(g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{% \prod_{(x:X)}}}A(x))}}}\mathchoice{\prod_{(x:X)}\,}{\mathchoice{{\textstyle% \prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{% \textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{% \mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x% :X)}}}P(x,g(x))$ as “there exists a choice function $g:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:% X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}A(x)$ such that for all $x:X$ we have $P(x,g(x))$”.

Thus, Theorem 2.15.7 (http://planetmath.org/215universalproperties#Thmprethm3) says that not only is the axiom of choice “true”, its antecedent   is actually equivalent      to its conclusion  . (On the other hand, the classical mathematician may find that (2.15.6) does not carry the usual meaning of the axiom of choice, since we have already specified the values of $g$, and there are no choices left to be made. We will return to this point in §3.8 (http://planetmath.org/38theaxiomofchoice).)

The above universal property for pair types is for “mapping in”, which is familiar from the category-theoretic notion of products    . However, pair types also have a universal property for “mapping out”, which may look less familiar. In the case of cartesian products, the non-dependent version simply expresses the cartesian closure   adjunction  :

 $\big{(}(A\times B)\to C\big{)}\;\simeq\;\big{(}A\to(B\to C)\big{)}.$

The dependent version of this is formulated for a type family $C:A\times B\to\mathcal{U}$:

 $\Bigl{(}\mathchoice{\prod_{w:A\times B}\,}{\mathchoice{{\textstyle\prod_{(w:A% \times B)}}}{\prod_{(w:A\times B)}}{\prod_{(w:A\times B)}}{\prod_{(w:A\times B% )}}}{\mathchoice{{\textstyle\prod_{(w:A\times B)}}}{\prod_{(w:A\times B)}}{% \prod_{(w:A\times B)}}{\prod_{(w:A\times B)}}}{\mathchoice{{\textstyle\prod_{(% w:A\times B)}}}{\prod_{(w:A\times B)}}{\prod_{(w:A\times B)}}{\prod_{(w:A% \times B)}}}C(w)\Bigr{)}\;\simeq\;\Bigl{(}\mathchoice{\prod_{(x:A)}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}\mathchoice{\prod_{(y:B)}\,}{\mathchoice{{\textstyle% \prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{% \textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{% \mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y% :B)}}}C(x,y)\Bigr{)}.$

Here the right-to-left function is simply the induction principle for $A\times B$, while the left-to-right is evaluation at a pair. We leave it to the reader to prove that these are quasi-inverses. There is also a version for $\Sigma$-types:

 $\Bigl{(}\mathchoice{\prod_{w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}B(x)}\,}{\mathchoice{{\textstyle\prod_{(w:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x))}}}{\prod_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}B(x))}}{\prod_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:% A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{% (x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\mathchoice{{\textstyle\prod_{(w:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\prod_{(w:\mathchoice{\sum_{x:A}\,}% {\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)% }}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x% :A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_% {(x:A)}}}B(x))}}{\prod_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}B(x))}}{\prod_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:% A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{% (x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\mathchoice{% {\textstyle\prod_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_% {(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\prod_{(w:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}{\prod_{(w:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x))}}{\prod_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}B(x))}}}C(w)\Bigr{)}\;\simeq\;\Bigl{(}\mathchoice{\prod_{(x:A)}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}\mathchoice{\prod_{(y:B(x))}\,}{\mathchoice{{\textstyle% \prod_{(y:B(x))}}}{\prod_{(y:B(x))}}{\prod_{(y:B(x))}}{\prod_{(y:B(x))}}}{% \mathchoice{{\textstyle\prod_{(y:B(x))}}}{\prod_{(y:B(x))}}{\prod_{(y:B(x))}}{% \prod_{(y:B(x))}}}{\mathchoice{{\textstyle\prod_{(y:B(x))}}}{\prod_{(y:B(x))}}% {\prod_{(y:B(x))}}{\prod_{(y:B(x))}}}C(x,y)\Bigr{)}.$ (2.15.9)

Again, the right-to-left function is the induction principle.

Some other induction principles are also part of universal properties of this sort. For instance, path induction is the right-to-left direction of an equivalence as follows:

 $\Bigl{(}\mathchoice{\prod_{(x:A)}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}\mathchoice{\prod% _{(p:a=x)}\,}{\mathchoice{{\textstyle\prod_{(p:a=x)}}}{\prod_{(p:a=x)}}{\prod_% {(p:a=x)}}{\prod_{(p:a=x)}}}{\mathchoice{{\textstyle\prod_{(p:a=x)}}}{\prod_{(% p:a=x)}}{\prod_{(p:a=x)}}{\prod_{(p:a=x)}}}{\mathchoice{{\textstyle\prod_{(p:a% =x)}}}{\prod_{(p:a=x)}}{\prod_{(p:a=x)}}{\prod_{(p:a=x)}}}B(x,p)\Bigr{)}\;% \simeq\;B(a,\mathsf{refl}_{a})$ (2.15.10)

for any $a:A$ and type family $B:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(a=x)\to\mathcal{U}$. However, inductive types with recursion, such as the natural numbers  , have more complicated universal properties; see http://planetmath.org/node/87578Chapter 5.

Since Theorem 2.15.2 (http://planetmath.org/215universalproperties#Thmprethm1) expresses the usual universal property of a cartesian product (in an appropriate homotopy-theoretic sense), the categorically inclined reader may well wonder about other limits and colimits  of types. In http://planetmath.org/node/87640Exercise 2.9 we ask the reader to show that the coproduct  type $A+B$ also has the expected universal property, and the nullary cases of $\mathbf{1}$ (the terminal object  ) and $\mathbf{0}$ (the initial object) are easy.

For pullbacks  , the expected explicit construction works: given $f:A\to C$ and $g:B\to C$, we define

 $A\times_{C}B:\!\!\equiv\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{\textstyle\sum% _{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle% \sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{% \textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}\mathchoice% {\sum_{(b:B)}\,}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:% B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{% (b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{% \sum_{(b:B)}}{\sum_{(b:B)}}}(f(a)=g(b)).$ (2.15.11)

In http://planetmath.org/node/87642Exercise 2.11 we ask the reader to verify this. Some more general homotopy limits can be constructed in a similar way, but for colimits we will need a new ingredient; see http://planetmath.org/node/87579Chapter 6.

Title 2.15 Universal properties
\metatable