# 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 counterexample, 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 $\mathscr{D}=(A,B,C,f,g)$ with $f:C\to{}A$ and $g:C\to{}B$.

###### Definition 7.4.2.

Given a span $\mathscr{D}=(A,B,C,f,g)$ and a type $D$, a cocone under $\mathscr{D}$ with base $D$ is a triple $(i,j,h)$ with $i:A\to{}D$, $j:B\to{}D$ and $h:\mathchoice{\prod_{c:C}\,}{\mathchoice{{\textstyle\prod_{(c:C)}}}{\prod_{(c:% C)}}{\prod_{(c:C)}}{\prod_{(c:C)}}}{\mathchoice{{\textstyle\prod_{(c:C)}}}{% \prod_{(c:C)}}{\prod_{(c:C)}}{\prod_{(c:C)}}}{\mathchoice{{\textstyle\prod_{(c% :C)}}}{\prod_{(c:C)}}{\prod_{(c:C)}}{\prod_{(c:C)}}}i(f(c))=j(g(c))$:

We denote by $\mathsf{cocone}_{\mathscr{D}}(D)$ the type of all such cocones.

The type of cocones is (covariantly) functorial. For instance, given $D,E$ and a map $t:D\to{}E$, there is a map

 $\left\{\begin{array}[]{rcl}\mathsf{cocone}_{\mathscr{D}}(D)&\longrightarrow&% \mathsf{cocone}_{\mathscr{D}}(E)\\ c&\longmapsto&t\circ c\end{array}\right.$

defined by:

 $t\circ(i,j,h)=(t\circ{}i,t\circ{}j,\mathsf{ap}_{t}\circ{}h)$

And given $D,E,F$, functions $t:D\to{}E$, $u:E\to{}F$ and $c:\mathsf{cocone}_{\mathscr{D}}(D)$, we have

 $\displaystyle\mathsf{id}_{D}\circ c$ $\displaystyle=c$ (7.4.3) $\displaystyle(u\circ{}t)\circ c$ $\displaystyle=u\circ(t\circ c).$ (7.4.4)
###### Definition 7.4.5.

Given a span $\mathscr{D}$ of $n$-types, an $n$-type $D$, and a cocone $c:\mathsf{cocone}_{\mathscr{D}}(D)$, the pair $(D,c)$ is said to be a pushout of $\mathscr{D}$ in $n$-types if for every $n$-type $E$, the map

 $\left\{\begin{array}[]{rcl}(D\to{}E)&\longrightarrow&\mathsf{cocone}_{\mathscr% {D}}(E)\\ t&\longmapsto&t\circ c\end{array}\right.$

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.

Let

be a span. We denote by $\mathopen{}\left\|\mathscr{D}\right\|_{n}\mathclose{}$ the following span of $n$-types:

###### Definition 7.4.7.

Let $D:\mathcal{U}$ and $c=(i,j,h):\mathsf{cocone}_{\mathscr{D}}(D)$. We define

 $\mathopen{}\left\|c\right\|_{n}\mathclose{}=(\mathopen{}\left\|i\right\|_{n}% \mathclose{},\mathopen{}\left\|j\right\|_{n}\mathclose{},\mathopen{}\left\|h% \right\|_{n}\mathclose{}):\mathsf{cocone}_{\mathopen{}\left\|\mathscr{D}\right% \|_{n}\mathclose{}}(\mathopen{}\left\|D\right\|_{n}\mathclose{})$

where $\mathopen{}\left\|h\right\|_{n}\mathclose{}:\mathopen{}\left\|i\right\|_{n}% \mathclose{}\circ\mathopen{}\left\|f\right\|_{n}\mathclose{}\sim\mathopen{}% \left\|j\right\|_{n}\mathclose{}\circ\mathopen{}\left\|g\right\|_{n}\mathclose{}$ 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.

Let

 $\includegraphics{HoTT_{f}ig_{7}.4.5.png}\qquad\text{and}\qquad\includegraphics% {HoTT_{f}ig_{7}.4.6.png}$

be spans. A map of spans $\mathscr{D}\to\mathscr{D}^{\prime}$ consists of functions $\alpha:A\to A^{\prime}$, $\beta:B\to B^{\prime}$, and $\gamma:C\to C^{\prime}$ and homotopies $\phi:\alpha\circ f\sim f^{\prime}\circ\gamma$ and $\psi:\beta\circ g\sim g^{\prime}\circ\gamma$.

Thus, for any span $\mathscr{D}$, we have a map of spans $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{\mathscr{D}}:\mathscr{D}\to% \mathopen{}\left\|\mathscr{D}\right\|_{n}\mathclose{}$ consisting of $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{A}$, $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{B}$, $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{C}$, and the naturality homotopies $\mathsf{nat}^{f}_{n}$ and $\mathsf{nat}^{g}_{n}$ from (7.3.4) (http://planetmath.org/73truncations#S0.E1).

We also need to know that maps of spans behave functorially. Namely, if $(\alpha,\beta,\gamma,\phi,\psi):\mathscr{D}\to\mathscr{D}^{\prime}$ is a map of spans and $D$ any type, then we have

 $\left\{\begin{array}[]{rcl}\mathsf{cocone}_{\mathscr{D}^{\prime}}(D)&% \longrightarrow&\mathsf{cocone}_{\mathscr{D}}(D)\\ (i,j,h)&\longmapsto&(i\circ\alpha,j\circ\beta,k)\end{array}\right.$

where $k:\mathchoice{\prod_{z:C}\,}{\mathchoice{{\textstyle\prod_{(z:C)}}}{\prod_{(z:% C)}}{\prod_{(z:C)}}{\prod_{(z:C)}}}{\mathchoice{{\textstyle\prod_{(z:C)}}}{% \prod_{(z:C)}}{\prod_{(z:C)}}{\prod_{(z:C)}}}{\mathchoice{{\textstyle\prod_{(z% :C)}}}{\prod_{(z:C)}}{\prod_{(z:C)}}{\prod_{(z:C)}}}i(\alpha(f(z)))=j(\beta(g(% z)))$ is the composite

 $\includegraphics{HoTT_{f}ig_{7}.4.7.png}$ (7.4.9)

We denote this cocone by $(i,j,h)\circ(\alpha,\beta,\gamma,\phi,\psi)$. Moreover, this functorial action commutes with the other functoriality of cocones:

###### Lemma 7.4.10.

Given $(\alpha,\beta,\gamma,\phi,\psi):\mathscr{D}\to\mathscr{D}^{\prime}$ and $t:D\to E$, the following diagram commutes:

###### Proof.

Given $(i,j,h):\mathsf{cocone}_{\mathscr{D}^{\prime}}(D)$, note that both composites yield a cocone whose first two components are $t\circ i\circ\alpha$ and $t\circ j\circ\beta$. 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 $(t\circ i,t\circ j,\mathsf{ap}_{t}\circ h)$:

(For brevity, we are omitting the parentheses around the arguments of functions.) On the other hand, for the left-bottom composite, the homotopy is $\mathsf{ap}_{t}$ applied to (7.4.9). Since $\mathsf{ap}$ respects path-concatenation, this is equal to

But $\mathsf{ap}_{t}\circ\mathsf{ap}_{i}=\mathsf{ap}_{t\circ i}$ and similarly for $j$, so these two homotopies are equal. ∎

Finally, note that since we defined $\mathopen{}\left\|c\right\|_{n}\mathclose{}:\mathsf{cocone}_{\mathopen{}\left% \|\mathscr{D}\right\|_{n}\mathclose{}}(\mathopen{}\left\|D\right\|_{n}% \mathclose{})$ using Lemma 7.3.5 (http://planetmath.org/73truncations#Thmprelem3), the additional condition (7.3.6) (http://planetmath.org/73truncations#S0.E2) implies

 $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{D}\circ c=\mathopen{}\left% \|c\right\|_{n}\mathclose{}\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_% {n}^{\mathscr{D}}.$ (7.4.11)

for any $c:\mathsf{cocone}_{\mathscr{D}}(D)$. Now we can prove our desired theorem.

###### Theorem 7.4.12.

Let $\mathscr{D}$ be a span and $(D,c)$ its pushout. Then $(\mathopen{}\left\|D\right\|_{n}\mathclose{},\mathopen{}\left\|c\right\|_{n}% \mathclose{})$ is a pushout of $\mathopen{}\left\|\mathscr{D}\right\|_{n}\mathclose{}$ in $n$-types.

###### Proof.

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 $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ c$ is an equivalence since $c$ is a pushout cocone. Thus, by the 2-out-of-3 property, to show that $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ\mathopen{}\left\|c\right\|_{n% }\mathclose{}$ 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:\mathopen{}\left\|D\right\|_{n}\mathclose{}\to E$; then

 $\displaystyle\big{(}t\circ\mathopen{}\left\|c\right\|_{n}\mathclose{}\big{)}% \circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{\mathscr{D}}$ $\displaystyle=t\circ\big{(}\mathopen{}\left\|c\right\|_{n}\mathclose{}\circ|% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{\mathscr{D}}\big{)}{}$ (by Lemma 7.4.10 (http://planetmath.org/74colimitsofntypeshmprelem2)) $\displaystyle=t\circ\big{(}|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{% D}\circ c\big{)}{}$ (by \eqref{eq:conetrunc}) $\displaystyle=\big{(}t\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{% D}\big{)}\circ 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 $\mathsf{happly}$:

 $\displaystyle\ell_{1}(i,j,p)$ $\displaystyle:\!\!\equiv(i,j,\mathsf{happly}(p))$ $\displaystyle\ell_{2}(i,j,p)$ $\displaystyle:\!\!\equiv(i,j,\mathsf{happly}(p))$

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

 $(i,j,p)\mapsto\big{(}i\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{% A},\;\;j\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{B},\;\;q\big{)}$

where $q$ is the composite

 $\displaystyle i\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{A}\circ f$ $\displaystyle=i\circ\mathopen{}\left\|f\right\|_{n}\mathclose{}\circ|\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{C}{}$ (by $\mathsf{funext}({\lambda}z.\,\mathsf{ap}_{i}(\mathsf{nat}^{f}_{n}(z)))$) $\displaystyle=j\circ\mathopen{}\left\|g\right\|_{n}\mathclose{}\circ|\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{C}{}$ (by $\mathsf{ap}_{\mathord{\hskip1.0pt\text{--}\hskip1.0pt}\circ|\mathord{\hskip1.0pt\text{--}\hskip1.0pt}|_{n}^{C}}(p)$) $\displaystyle=j\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{B}\circ g% .{}$ (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

 $\mathsf{happly}(q,z):i(\mathopen{}\left|f(z)\right|_{n}\mathclose{})=j(% \mathopen{}\left|g(z)\right|_{n}\mathclose{})$

(with $q$ as above) is equal to the composite

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

However, since $\mathsf{happly}$ is functorial, it suffices to check equality for the three component paths:

 $\displaystyle\mathsf{happly}({\mathsf{funext}({\lambda}z.\,\mathsf{ap}_{i}(% \mathsf{nat}^{f}_{n}(z)))},z)$ $\displaystyle={\mathsf{ap}_{i}(\mathsf{nat}^{f}_{n}(z))}$ $\displaystyle\mathsf{happly}(\mathsf{ap}_{\mathord{\hskip 1.0pt\text{--}\hskip 1% .0pt}\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}^{C}}(p),z)$ $\displaystyle={\mathsf{happly}(p,\mathopen{}\left|z\right|_{n}\mathclose{})}$ $\displaystyle\mathsf{happly}({\mathsf{funext}({\lambda}z.\,\mathsf{ap}_{j}(% \mathsf{nat}^{g}_{n}(z)))},z)$ $\displaystyle={\mathsf{ap}_{j}(\mathsf{nat}^{g}_{n}(z))}.$

The first and third of these are just the fact that $\mathsf{happly}$ is quasi-inverse to $\mathsf{funext}$, while the second is an easy general lemma about $\mathsf{happly}$ and precomposition. ∎

Title 7.4 Colimits of n-types
\metatable