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
(2.15.1) |
defined by .
Theorem 2.15.2.
(2.15.1) is an equivalence.
Proof.
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
(2.15.3) |
By Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1), for any we have . Thus, by function extensionality, the function (2.15.3) is equal to .
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
(2.15.4) |
defined as before by .
Theorem 2.15.5.
(2.15.4) is an equivalence.
Proof.
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) |
Note that if we have for some , 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 to the function . Now given , the round-trip composite yields the function
(2.15.8) |
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. ∎
This is noteworthy because the propositions-as-types interpretation of (2.15.6) is “the axiom of choice
”.
If we read as “there exists” and (sometimes) as “for all”, we can pronounce:
-
•
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:
(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:
(2.15.10) |
for any and type family .
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 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
(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 |