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

HoTT_fig_7.4.1.png

Definition 7.4.2.

Given a span $\mathrm{D}\mathrm{=}\mathrm{(}A\mathrm{,}B\mathrm{,}C\mathrm{,}f\mathrm{,}g\mathrm{)}$ and a type $D$, a cocone under $\mathrm{D}$ with base $\mathrm{D}$ is a triple $\mathrm{(}i\mathrm{,}j\mathrm{,}h\mathrm{)}$ with $i\mathrm{:}A\mathrm{\to }D$, $j\mathrm{:}B\mathrm{\to }D$ and $h\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}c\mathrm{:}C\mathrm{)}}i\mathit{}\mathrm{(}f\mathit{}\mathrm{(}c\mathrm{)}\mathrm{)}\mathrm{=}j\mathit{}\mathrm{(}g\mathit{}\mathrm{(}c\mathrm{)}\mathrm{)}$:

HoTT_fig_7.4.2.png

We denote by ${\mathrm{cocone}}_{\mathrm{D}}\mathit{}\mathrm{(}D\mathrm{)}$ 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

defined by:

$$t\circ (i,j,h)=(t\circ i,t\circ j,{\mathrm{𝖺𝗉}}_t\circ h)$$

And given $D,E,F$, functions $t:D\to E$, $u:E\to F$ and $c:{\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{𝒟}(D)$, we have

${\mathrm{𝗂𝖽}}_D\circ c$ $=c$ (7.4.3)

$(u\circ t)\circ c$ $=u\circ (t\circ c).$ (7.4.4)

Definition 7.4.5.

Given a span $\mathrm{D}$ of $n$-types, an $n$-type $D$, and a cocone $c\mathrm{:}{\mathrm{cocone}}_{\mathrm{D}}\mathit{}\mathrm{(}D\mathrm{)}$, the pair $\mathrm{(}D\mathrm{,}c\mathrm{)}$ is said to be a pushout of $\mathrm{D}$ in $\mathrm{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.

Let

HoTT_fig_7.4.3.png

be a span. We denote by ${\mathrm{\parallel }\mathrm{D}\mathrm{\parallel }}_n$ the following span of $n$-types:

HoTT_fig_7.4.4.png

Definition 7.4.7.

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

$$\parallel c{\parallel }_n=(\parallel i{\parallel }_n,\parallel j{\parallel }_n,\parallel h{\parallel }_n):{\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{\parallel 𝒟{\parallel }_n}(\parallel D{\parallel }_n)$$

where $\mathrm{\parallel }h{\mathrm{\parallel }}_n\mathrm{:}\mathrm{\parallel }i{\mathrm{\parallel }}_n\mathrm{\circ }\mathrm{\parallel }f{\mathrm{\parallel }}_n\mathrm{\sim }\mathrm{\parallel }j{\mathrm{\parallel }}_n\mathrm{\circ }\mathrm{\parallel }g{\mathrm{\parallel }}_n$ 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

$$HoT{T}_{f}i{g}_7\mathrm{.4.5}.png\mathit{\hspace{1em}\hspace{1em}}\text{𝑎𝑛𝑑}\mathit{\hspace{1em}\hspace{1em}}HoT{T}_{f}i{g}_7\mathrm{.4.6}.png$$

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

Thus, for any span $𝒟$, we have a map of spans $|\text{–}{|}_n^{𝒟}:𝒟\to \parallel 𝒟{\parallel }_n$ consisting of ${|\text{–}|}_n^A$, ${|\text{–}|}_n^B$, ${|\text{–}|}_n^C$, and the naturality homotopies ${\mathrm{𝗇𝖺𝗍}}_n^f$ and ${\mathrm{𝗇𝖺𝗍}}_n^g$ 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 ,\varphi ,\psi ):𝒟\to {𝒟}^{\prime }$ is a map of spans and $D$ any type, then we have

where $k:{\prod }_{(z:C)}i(\alpha (f(z)))=j(\beta (g(z)))$ is the composite

$$HoT{T}_{f}i{g}_7\mathrm{.4.7}.png$$ (7.4.9)

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

Lemma 7.4.10.

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

HoTT_fig_7.4.8.png

Proof.

Given $(i,j,h):{\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{{𝒟}^{\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,{\mathrm{𝖺𝗉}}_t\circ h)$:

HoTT_fig_7.4.9.png

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

HoTT_fig_7.4.10.png

But ${\mathrm{𝖺𝗉}}_t\circ {\mathrm{𝖺𝗉}}_i={\mathrm{𝖺𝗉}}_{t\circ i}$ and similarly for $j$, so these two homotopies are equal. ∎

Finally, note that since we defined $\parallel c{\parallel }_n:{\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{\parallel 𝒟{\parallel }_n}(\parallel D{\parallel }_n)$ using Lemma 7.3.5 (http://planetmath.org/73truncations#Thmprelem3), the additional condition (7.3.6) (http://planetmath.org/73truncations#S0.E2) implies

$$|\text{–}{|}_n^D\circ c=\parallel c{\parallel }_n\circ |\text{–}{|}_n^{𝒟}.$$ (7.4.11)

for any $c:{\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{𝒟}(D)$. Now we can prove our desired theorem.

Theorem 7.4.12.

Let $\mathrm{D}$ be a span and $\mathrm{(}D\mathrm{,}c\mathrm{)}$ its pushout. Then $\mathrm{(}\mathrm{\parallel }D{\mathrm{\parallel }}_n\mathrm{,}\mathrm{\parallel }c{\mathrm{\parallel }}_n\mathrm{)}$ is a pushout of ${\mathrm{\parallel }\mathrm{D}\mathrm{\parallel }}_n$ in $n$-types.

Proof.

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

HoTT_fig_7.4.11.png

The upper horizontal arrow is an equivalence since $E$ is an $n$-type, while $\text{–}\circ c$ is an equivalence since $c$ is a pushout cocone. Thus, by the 2-out-of-3 property, to show that $\text{–}\circ \parallel c{\parallel }_n$ 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:\parallel D{\parallel }_n\to E$; then

$(t\circ \parallel c{\parallel }_n)\circ |\text{–}{|}_n^{𝒟}$ $=t\circ (\parallel c{\parallel }_n\circ |\text{–}{|}_n^{𝒟})$ (by Lemma 7.4.10 (http://planetmath.org/74colimitsofntypeshmprelem2))

$=t\circ \left({|\text{–}|}_n^D\circ c\right)$ (by $\eqref{eq:conetrunc}$)

$=\left(t\circ {|\text{–}|}_n^D\right)\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 $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}$:

${\mathrm{\ell }}_1(i,j,p)$ $:\equiv (i,j,\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(p))$

${\mathrm{\ell }}_2(i,j,p)$ $:\equiv (i,j,\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(p))$

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

$$(i,j,p)\mapsto (i\circ {|\text{–}|}_n^A,j\circ {|\text{–}|}_n^B,q)$$

where $q$ is the composite

$i\circ {|\text{–}|}_n^A\circ f$ $=i\circ \parallel f{\parallel }_n\circ |\text{–}{|}_n^C$ (by $\mathsf{funext}({\lambda}z.\,\mathsf{ap}_{i}(\mathsf{nat}^{f}_{n}(z)))$)

$=j\circ \parallel g{\parallel }_n\circ |\text{–}{|}_n^C$ (by $\mathsf{ap}_{\mathord{\hskip1.0pt\text{--}\hskip1.0pt}\circ|\mathord{\hskip1.0pt\text{--}\hskip1.0pt}|_{n}^{C}}(p)$)

$=j\circ {|\text{–}|}_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

$$\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(q,z):i(|f(z){|}_n)=j(|g(z){|}_n)$$

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

$i(|f(z){|}_n)$ $=i(\parallel f{\parallel }_n(|z{|}_n))$ (by $\mathsf{ap}_{i}(\mathsf{nat}^{f}_{n}(z))$)

$=j(\parallel g{\parallel }_n(|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 $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}$ is functorial, it suffices to check equality for the three component paths:

$\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(\mathrm{𝖿𝗎𝗇𝖾𝗑𝗍}(\lambda z.{\mathrm{𝖺𝗉}}_i({\mathrm{𝗇𝖺𝗍}}_n^f(z))),z)$ $={\mathrm{𝖺𝗉}}_i({\mathrm{𝗇𝖺𝗍}}_n^f(z))$

$\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}({\mathrm{𝖺𝗉}}_{\text{–}\circ {|\text{–}|}_n^C}(p),z)$ $=\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(p,|z{|}_n)$

$\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(\mathrm{𝖿𝗎𝗇𝖾𝗑𝗍}(\lambda z.{\mathrm{𝖺𝗉}}_j({\mathrm{𝗇𝖺𝗍}}_n^g(z))),z)$ $={\mathrm{𝖺𝗉}}_j({\mathrm{𝗇𝖺𝗍}}_n^g(z)).$

The first and third of these are just the fact that $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}$ is quasi-inverse to $\mathrm{𝖿𝗎𝗇𝖾𝗑𝗍}$, while the second is an easy general lemma about $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}$ and precomposition. ∎

Title	7.4 Colimits of n-types