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 n-types may no longer be an n-type (for an extreme counterexampleMathworldPlanetmath, see http://planetmath.org/node/87811Exercise 7.2). However, if we n-truncate it, we obtain an n-type which satisfies the correct universal property with respect to other n-types.

In this section we prove this for pushouts, which are the most important and nontrivial case of colimits. Recall the following definitions from §6.8 (http://planetmath.org/68pushouts).

Definition 7.4.1.

A span is a 5-tuple D=(A,B,C,f,g) with f:CA and g:CB.



Definition 7.4.2.

Given a span D=(A,B,C,f,g) and a type D, a cocone under D with base D is a triple (i,j,h) with i:AD, j:BD and h:(c:C)i(f(c))=j(g(c)):



We denote by coconeD(D) the type of all such cocones.

The type of cocones is (covariantly) functorial. For instance, given D,E and a map t:DE, there is a map


defined by:


And given D,E,F, functions t:DE, u:EF and c:𝖼𝗈𝖼𝗈𝗇𝖾𝒟(D), we have

𝗂𝖽Dc =c (7.4.3)
(ut)c =u(tc). (7.4.4)
Definition 7.4.5.

Given a span D of n-types, an n-type D, and a cocone c:coconeD(D), the pair (D,c) is said to be a pushout of D in n-types if for every n-type E, the map


is an equivalence.

In order to construct pushouts of n-types, we need to explain how to reflect spans and cocones.

Definition 7.4.6.




be a span. We denote by Dn the following span of n-types:



Definition 7.4.7.

Let D:U and c=(i,j,h):coconeD(D). We define


where hn:infnjngn is defined as in Lemma 7.3.5 (http://planetmath.org/73truncations#Thmprelem3).

We now observe that the maps from each type to its n-truncation assemble into a map of spans, in the following sense.

Definition 7.4.8.


\includegraphicsHoTTfig7.4.5.png  𝑎𝑛𝑑  \includegraphicsHoTTfig7.4.6.png

be spans. A map of spans DD consists of functions α:AA, β:BB, and γ:CC and homotopies ϕ:αffγ and ψ:βggγ.

Thus, for any span 𝒟, we have a map of spans ||n𝒟:𝒟𝒟n consisting of ||nA, ||nB, ||nC, and the naturality homotopies 𝗇𝖺𝗍nf and 𝗇𝖺𝗍ng 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 D any type, then we have


where k:(z:C)i(α(f(z)))=j(β(g(z))) is the composite

\includegraphicsHoTTfig7.4.7.png (7.4.9)

We denote this cocone by (i,j,h)(α,β,γ,ϕ,ψ). Moreover, this functorial action commutes with the other functoriality of cocones:

Lemma 7.4.10.

Given (α,β,γ,ϕ,ψ):DD and t:DE, the following diagram commutes:




Given (i,j,h):𝖼𝗈𝖼𝗈𝗇𝖾𝒟(D), note that both composites yield a cocone whose first two components are tiα and tjβ. Thus, it remains to verify that the homotopies agree. For the top-right composite, the homotopy is (7.4.9) with (i,j,h) replaced by (ti,tj,𝖺𝗉th):



(For brevity, we are omitting the parentheses around the arguments of functions.) On the other hand, for the left-bottom composite, the homotopy is 𝖺𝗉t applied to (7.4.9). Since 𝖺𝗉 respects path-concatenation, this is equal to



But 𝖺𝗉t𝖺𝗉i=𝖺𝗉ti and similarly for j, so these two homotopies are equal. ∎

Finally, note that since we defined cn:𝖼𝗈𝖼𝗈𝗇𝖾𝒟n(Dn) using Lemma 7.3.5 (http://planetmath.org/73truncations#Thmprelem3), the additional condition (7.3.6) (http://planetmath.org/73truncations#S0.E2) implies

||nDc=cn||n𝒟. (7.4.11)

for any c:𝖼𝗈𝖼𝗈𝗇𝖾𝒟(D). Now we can prove our desired theoremMathworldPlanetmath.

Theorem 7.4.12.

Let D be a span and (D,c) its pushout. Then (Dn,cn) is a pushout of Dn in n-types.


Let E be an n-type, and consider the following diagram:



The upper horizontal arrow is an equivalence since E is an n-type, while c is an equivalence since c is a pushout cocone. Thus, by the 2-out-of-3 property, to show that cn 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 t:DnE; then

(tcn)||n𝒟 =t(cn||n𝒟) (by Lemma 7.4.10 (http://planetmath.org/74colimitsofntypeshmprelem2))
=t(||nDc) (by \eqref{eq:conetrunc})
=(t||nD)c. (by \eqref{eq:composeconefunc})

To show that the middle horizontal arrow is an equivalence, consider the lower square. The two lower vertical arrows are simply applications of 𝗁𝖺𝗉𝗉𝗅𝗒:

1(i,j,p) :(i,j,𝗁𝖺𝗉𝗉𝗅𝗒(p))
2(i,j,p) :(i,j,𝗁𝖺𝗉𝗉𝗅𝗒(p))

and hence are equivalences by function extensionality. The lowest horizontal arrow is defined by


where q is the composite

i||nAf =ifn||nC (by $\mathsf{funext}({\lambda}z.\,\mathsf{ap}_{i}(\mathsf{nat}^{f}_{n}(z)))$)
=jgn||nC (by $\mathsf{ap}_{\mathord{\hskip1.0pt\text{--}\hskip1.0pt}\circ|\mathord{\hskip1.0pt\text{--}\hskip1.0pt}|_{n}^{C}}(p)$)
=j||nBg. (by $\mathsf{funext}({\lambda}z.\,\mathsf{ap}_{j}(\mathsf{nat}^{g}_{n}(z)))$)

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 (i,j,p) in the lower left corner and z:C, the path


(with q as above) is equal to the composite

i(|f(z)|n) =i(fn(|z|n)) (by $\mathsf{ap}_{i}(\mathsf{nat}^{f}_{n}(z))$)
=j(gn(|z|n)) (by $\mathsf{happly}(p,\mathopen{}\left|z\right|_{n}\mathclose{})$)
=j(|g(z)|n). (by $\mathsf{ap}_{j}(\mathsf{nat}^{g}_{n}(z))$)

However, since 𝗁𝖺𝗉𝗉𝗅𝗒 is functorial, it suffices to check equality for the three component paths:

𝗁𝖺𝗉𝗉𝗅𝗒(𝖿𝗎𝗇𝖾𝗑𝗍(λz.𝖺𝗉i(𝗇𝖺𝗍nf(z))),z) =𝖺𝗉i(𝗇𝖺𝗍nf(z))
𝗁𝖺𝗉𝗉𝗅𝗒(𝖺𝗉||nC(p),z) =𝗁𝖺𝗉𝗉𝗅𝗒(p,|z|n)
𝗁𝖺𝗉𝗉𝗅𝗒(𝖿𝗎𝗇𝖾𝗑𝗍(λz.𝖺𝗉j(𝗇𝖺𝗍ng(z))),z) =𝖺𝗉j(𝗇𝖺𝗍ng(z)).

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