202508311908

Tags : Homotopy Type Theory

Truncations Preserve Products

---

Theorem

For any types $A,B$ the induced map $\Vert A\times B{\Vert }_n\to \Vert A{\Vert }_n\times \Vert B{\Vert }_n$ is an equivalence.

We can show this by showing that it suffices the universal property of the product.

$$\begin{array}{rl}(\Vert A{\Vert }_n\times \Vert B{\Vert }_n\to C)& =(\Vert A{\Vert }_n\to (\Vert B{\Vert }_n\to C))\\ & =(\Vert A{\Vert }_n\to (B\to C))\\ & =(A\to (B\to C))\\ & =A\times B\to C\\ & =\Vert A\times B{\Vert }_n\to C\end{array}$$

where $C$ is an $n$-type.

---

References