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({𝕊}^1)$ in sec:pi1-s1-intro.There is also a more homotopy-theoretic approach; see ex:rezk-vankampen.

We need a more refined version of the encode-decode method.In sec:pi1-s1-intro (as well as in sec:compute-coprod,sec: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 $\mathrm{\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 ${\mathrm{\Pi }}_{1}X:X\to X\to 𝒰$ for the $0$-truncation of its identity type, i.e. ${\mathrm{\Pi }}_{1}X(x,y):\equiv \parallel x=y{\parallel }_0$.Note that we have induced groupoid operations

$(\text{–}\text{–})$$\mathrm{\hspace{0.33em}}:{\mathrm{\Pi }}_{1}X(x,y)\to {\mathrm{\Pi }}_{1}X(y,z)\to {\mathrm{\Pi }}_{1}X(x,z)$

${(\text{–})}^{-1}$$\mathrm{\hspace{0.33em}}:{\mathrm{\Pi }}_{1}X(x,y)\to {\mathrm{\Pi }}_{1}X(y,x)$

${\mathrm{𝗋𝖾𝖿𝗅}}_x$$\mathrm{\hspace{0.33em}}:{\mathrm{\Pi }}_{1}X(x,x)$

${\mathrm{𝖺𝗉}}_f$$\mathrm{\hspace{0.33em}}:{\mathrm{\Pi }}_{1}X(x,y)\to {\mathrm{\Pi }}_{1}Y(fx,fy)$

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