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.

In this section we will describe a proof of the van Kampen theorem which uses the same encode-decode method that we used for $\pi_{1}(\mathbb{S}^{1})$ in \autorefsec:pi1-s1-intro. There is also a more homotopy-theoretic approach; see \autorefex:rezk-vankampen.

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