202509222009

Tags : Homotopy Type Theory

n-truncation of a pushout is a pushout in n-types

---

Theorem

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

To show this, we need to show that this satisfies the universal property of pushouts.

Consider the following diagram where $E$ is an $n$-type

The upper horizontal arrow is an equivalence since $E$ is an $n$-type. The right, downwards arrow is an equivalence since $c$ is a pushout.

by the 2 out of 3 property, we need to show that the middle horizontal arrow is an equivalence and the upper square commutes to show that the left downward arrow is an equivalence.

To show that the upper square commutes:

$$\begin{array}{rl}(t\circ \Vert c{\Vert }_n)\circ |-{|}_n^{\mathcal{D}}& =t\circ (\Vert c{\Vert }_n\circ |-{|}_n^{\mathcal{D}})\\ & =t\circ (|-{|}_n^D\circ c)\\ & =(t\circ |-{|}_n^D)\circ c\end{array}$$

The last line is by functoriality of truncations, the first equality if by the theorem proved in Maps between Cocones.

Now we need to show that the middle horizontal arrow is an equivalence, for that, we look at the bottom square. Both vertical arrows are equivalence as they are just an application of $\text{happly}$. And now we are only left to show that the bottom arrow is an equivalence:

$$(i,j,p)⟼(i\circ |-{|}_n^A,j\circ |-{|}_n^B,q)$$

we have that the lower square commutes definitionally on the first two components.

So we need to show that $q$ is equal to:

$$\begin{array}{rl}i(|f(z){|}_n)& =i(\Vert f{\Vert }_n(|z{|}_n))\\ & =j(\Vert g{\Vert }_n(|z{|}_n))\\ & =j(|g(z){|}_n)\end{array}$$

This is trivial, so by 2 out of 3 rule, the lower arrow is an equivalence, so the lower square commutes, so the middle horizontal arrow is an equivalence and the upper square commutes so the left downward arrow is an equivalence, and we are done.

---

References

• Pushouts (HoTT)
• Pushouts of n-types
• n-Types
• Maps between Cocones