Homotopy Type Theory Seifert-van Kampen theorem > history (Rev #2, changes)

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}$

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:

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

• agda formalisation
• lean formalisation

References

• HoTT book