7.4 Colimits of n-types
Recall that in §6.8 (http://planetmath.org/68pushouts), we used higher inductive types to define pushouts of types, and proved their universal property. In general, a (homotopy) colimit of -types may no longer be an -type (for an extreme counterexample, see http://planetmath.org/node/87811Exercise 7.2). However, if we -truncate it, we obtain an -type which satisfies the correct universal property with respect to other -types.
A span is a 5-tuple with and .
Given a span and a type , a cocone under with base is a triple with , and :
We denote by the type of all such cocones.
The type of cocones is (covariantly) functorial. For instance, given and a map , there is a map
And given , functions , and , we have
Given a span of -types, an -type , and a cocone , the pair is said to be a pushout of in -types if for every -type , the map
is an equivalence.
In order to construct pushouts of -types, we need to explain how to reflect spans and cocones.
be a span. We denote by the following span of -types:
Let and . We define
where is defined as in Lemma 7.3.5 (http://planetmath.org/73truncations#Thmprelem3).
We now observe that the maps from each type to its -truncation assemble into a map of spans, in the following sense.
be spans. A map of spans consists of functions , , and and homotopies and .
Thus, for any span , we have a map of spans consisting of , , , and the naturality homotopies and from (7.3.4) (http://planetmath.org/73truncations#S0.E1).
We also need to know that maps of spans behave functorially. Namely, if is a map of spans and any type, then we have
where is the composite
We denote this cocone by . Moreover, this functorial action commutes with the other functoriality of cocones:
Given and , the following diagram commutes:
Given , note that both composites yield a cocone whose first two components are and . Thus, it remains to verify that the homotopies agree. For the top-right composite, the homotopy is (7.4.9) with replaced by :
(For brevity, we are omitting the parentheses around the arguments of functions.) On the other hand, for the left-bottom composite, the homotopy is applied to (7.4.9). Since respects path-concatenation, this is equal to
But and similarly for , so these two homotopies are equal. ∎
Finally, note that since we defined using Lemma 7.3.5 (http://planetmath.org/73truncations#Thmprelem3), the additional condition (7.3.6) (http://planetmath.org/73truncations#S0.E2) implies
for any . Now we can prove our desired theorem.
Let be a span and its pushout. Then is a pushout of in -types.
Let be an -type, and consider the following diagram:
The upper horizontal arrow is an equivalence since is an -type, while is an equivalence since is a pushout cocone. Thus, by the 2-out-of-3 property, to show that is an equivalence, it will suffice to show that the upper square commutes and that the middle horizontal arrow is an equivalence. To see that the upper square commutes, let ; then
|(by Lemma 7.4.10 (http://planetmath.org/74colimitsofntypeshmprelem2))|
To show that the middle horizontal arrow is an equivalence, consider the lower square. The two lower vertical arrows are simply applications of :
and hence are equivalences by function extensionality. The lowest horizontal arrow is defined by
where is the composite
This is an equivalence, because it is induced by an equivalence of cospans. Thus, by 2-out-of-3, it will suffice to show that the lower square commutes. But the two composites around the lower square agree definitionally on the first two components, so it suffices to show that for in the lower left corner and , the path
(with as above) is equal to the composite
However, since is functorial, it suffices to check equality for the three component paths:
The first and third of these are just the fact that is quasi-inverse to , while the second is an easy general lemma about and precomposition. ∎
|Title||7.4 Colimits of n-types|