# 8.7 The van Kampen theorem

The van Kampen theorem  calculates the fundamental group   $\pi_{1}$ of a (homotopy   ) pushout of spaces. It is traditionally stated for a topological space  $X$ which is the union of two open subspaces $U$ and $V$, but in homotopy-theoretic terms this is just a convenient way of ensuring that $X$ is the pushout of $U$ and $V$ over their intersection   . Thus, we will prove a version of the van Kampen theorem for arbitrary pushouts.

We need a more refined version of the encode-decode method. In \autorefsec:pi1-s1-intro (as well as in \autorefsec:compute-coprod,\autorefsec:compute-nat) we used it to characterize the path space of a (higher) inductive type $W$ — deriving as a consequence a characterization of the loop space  $\Omega(W)$, and thereby also of its 0-truncation $\pi_{1}(W)$. In the van Kampen theorem, our goal is only to characterize the fundamental group $\pi_{1}(W)$, and we do not have any explicit description of the loop spaces or the path spaces to use.

It turns out that we can use the same technique directly for a truncated version of the path fibration  , thereby characterizing not only the fundamental group $\pi_{1}(W)$, but also the whole fundamental groupoid      . Specifically, for a type $X$, write $\Pi_{1}X:X\to X\to\mathcal{U}$ for the $0$-truncation of its identity type, i.e. $\Pi_{1}X(x,y):\!\!\equiv\mathopen{}\left\|x=y\right\|_{0}\mathclose{}$. Note that we have induced groupoid operations  $\displaystyle(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt})$ $\displaystyle\;:\;\Pi_{1}X(x,y)\to\Pi_{1}X(y,z)\to\Pi_{1}X(x,z)$ $\displaystyle\mathord{{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}^{-1}}$ $\displaystyle\;:\;\Pi_{1}X(x,y)\to\Pi_{1}X(y,x)$ $\displaystyle\mathsf{refl}_{x}$ $\displaystyle\;:\;\Pi_{1}X(x,x)$ $\displaystyle\mathsf{ap}_{f}$ $\displaystyle\;:\;\Pi_{1}X(x,y)\to\Pi_{1}Y(fx,fy)$

for which we use the same notation as the corresponding operations on paths.

Title 8.7 The van Kampen theorem
\metatable