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 , we have a function
defined by .
(2.15.1) is an equivalence.
We define the quasi-inverse by sending to . (Technically, we have used the induction principle for the cartesian product , to reduce to the case of a pair. From now on we will often apply this principle without explicit mention.)
Now given , the round-trip composite yields the function
On the other hand, given , the round-trip composite yields the pair . By the uniqueness principle for functions, this is (judgmentally) equal to . ∎
In fact, we also have a dependently typed version of this universal property. Suppose given a type and type families . Then we have a function
defined as before by .
(2.15.4) is an equivalence.
Left to the reader. ∎
Just as -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 and type families and . Then we have a function
(2.15.6) is an equivalence.
As before, we define a quasi-inverse to send to the function . Now given , the round-trip composite yields the function
Now for any , by Corollary 2.7.3 (http://planetmath.org/27sigmatypes#Thmprecor1) (the uniqueness principle for -types) we have
Thus, by function extensionality, (2.15.8) is equal to . On the other hand, given , the round-trip composite yields , which is judgmentally equal to as before. ∎
as “for all there exists an such that ”, and
as “there exists a choice function such that for all we have ”.
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 , 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:
The dependent version of this is formulated for a type family :
Here the right-to-left function is simply the induction principle for , 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 -types:
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:
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 also has the expected universal property, and the nullary cases of (the terminal object) and (the initial object) are easy.
For pullbacks, the expected explicit construction works: given and , we define
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|