2.15 Universal properties
By combining the path computation rules described in the preceding sections^{}, we can show that various type forming operations^{} satisfy the expected universal properties^{}, interpreted in a homotopical way as equivalences. For instance, given types $X,A,B$, we have a function
$$(X\to A\times B)\to (X\to A)\times (X\to B)$$  (2.15.1) 
defined by $f\mapsto ({\mathrm{\U0001d5c9\U0001d5cb}}_{1}\circ f,{\mathrm{\U0001d5c9\U0001d5cb}}_{2}\circ f)$.
Theorem 2.15.2.
(2.15.1) is an equivalence.
Proof.
We define the quasiinverse^{} by sending $(g,h)$ to $\lambda x.(g(x),h(x))$. (Technically, we have used the induction^{} principle for the cartesian product^{} $(X\to A)\times (X\to B)$, to reduce to the case of a pair. From now on we will often apply this principle without explicit mention.)
Now given $f:X\to A\times B$, the roundtrip composite yields the function
$$\lambda x.({\mathrm{\U0001d5c9\U0001d5cb}}_{1}(f(x)),{\mathrm{\U0001d5c9\U0001d5cb}}_{2}(f(x))).$$  (2.15.3) 
By Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1), for any $x:X$ we have $({\mathrm{\U0001d5c9\U0001d5cb}}_{1}(f(x)),{\mathrm{\U0001d5c9\U0001d5cb}}_{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 roundtrip 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
$$\left(\prod _{x:X}(A(x)\times B(x))\right)\to \left(\prod _{x:X}A(x)\right)\times \left(\prod _{x:X}B(x)\right)$$  (2.15.4) 
defined as before by $f\mapsto ({\mathrm{\U0001d5c9\U0001d5cb}}_{1}\circ f,{\mathrm{\U0001d5c9\U0001d5cb}}_{2}\circ f)$.
Theorem 2.15.5.
(2.15.4) is an equivalence.
Proof.
Left to the reader. ∎
Just as $\mathrm{\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:{\prod}_{(x:X)}A(x)\to \mathcal{U}$. Then we have a function
$$\left(\prod _{x:X}\sum _{(a:A(x))}P(x,a)\right)\to \left(\sum _{(g:{\prod}_{(x:X)}A(x))}\prod _{(x:X)}P(x,g(x))\right).$$  (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 quasiinverse to send $(g,h)$ to the function $\lambda x.(g(x),h(x))$. Now given $f:{\prod}_{(x:X)}{\sum}_{(a:A(x))}P(x,a)$, the roundtrip composite yields the function
$$\lambda x.({\mathrm{\U0001d5c9\U0001d5cb}}_{1}(f(x)),{\mathrm{\U0001d5c9\U0001d5cb}}_{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 $\mathrm{\Sigma}$types) we have
$$({\mathrm{\U0001d5c9\U0001d5cb}}_{1}(f(x)),{\mathrm{\U0001d5c9\U0001d5cb}}_{2}(f(x)))=f(x).$$ 
Thus, by function extensionality, (2.15.8) is equal to $f$. On the other hand, given $(g,h)$, the roundtrip composite yields $(\lambda x.g(x),\lambda x.h(x))$, which is judgmentally equal to $(g,h)$ as before. ∎
This is noteworthy because the propositionsastypes interpretation^{} of (2.15.6) is “the axiom of choice^{}”. If we read $\mathrm{\Sigma}$ as “there exists” and $\mathrm{\Pi}$ (sometimes) as “for all”, we can pronounce:

•
${\prod}_{(x: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

•
${\sum}_{(g:{\prod}_{(x:X)}A(x))}{\prod}_{(x:X)}P(x,g(x))$ as “there exists a choice function $g:{\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 categorytheoretic 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 nondependent version simply expresses the cartesian closure^{} adjunction^{}:
$$((A\times B)\to C)\simeq (A\to (B\to C)).$$ 
The dependent version of this is formulated for a type family $C:A\times B\to \mathcal{U}$:
$$\left(\prod _{w:A\times B}C(w)\right)\simeq \left(\prod _{(x:A)}\prod _{(y:B)}C(x,y)\right).$$ 
Here the righttoleft function is simply the induction principle for $A\times B$, while the lefttoright is evaluation at a pair. We leave it to the reader to prove that these are quasiinverses. There is also a version for $\mathrm{\Sigma}$types:
$$\left(\prod _{w:{\sum}_{(x:A)}B(x)}C(w)\right)\simeq \left(\prod _{(x:A)}\prod _{(y:B(x))}C(x,y)\right).$$  (2.15.9) 
Again, the righttoleft function is the induction principle.
Some other induction principles are also part of universal properties of this sort. For instance, path induction is the righttoleft direction of an equivalence as follows:
$$\left(\prod _{(x:A)}\prod _{(p:a=x)}B(x,p)\right)\simeq B(a,{\mathrm{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{a})$$  (2.15.10) 
for any $a:A$ and type family $B:{\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 homotopytheoretic 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 $\mathrm{\U0001d7cf}$ (the terminal object^{}) and $\mathrm{\U0001d7ce}$ (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 \sum _{(a:A)}\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 