Homotopy Type Theory Seifert-van Kampen theorem

Idea

The van Kampen theorem calculates the fundamental group $\pi_1$ of a 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 a convenient way of ensuring that $X$ is the pushout of $U$ and $V$ over their intersection.

Groupoids

It is useful to generalise the fundamental group $\pi_1(-)\equiv \| \Omega(-) \|_0$ of a type $X$ to the fundamental groupoid $\Pi_1 X : X \to X \to \mathcal{U}$

$\Pi_1 X (x, y) \equiv \| x = y \|_0$

This has induced groupoid operations coming from the identity type: concatenation, inverses, identity and function application.

Theorem

Let $A, B, C$ be types? and $f : A \to B$ and $g : A \to C$ functions?. Let $P\equiv B \sqcup_A C$ be their pushout.

By defining a special code function the statement of the theorem becomes:

$\Pi_1 P(u, v) \simeq code(u,v)$

this is the encode-decode method?.

Code

There are (at least) two code functions that can be given. These are listed in the HoTT Book section 8.7. The first is a “naive” van Kampen theorem. The second version is the van Kampen at a set of basepoints.

Formalisation

category: homotopy theory