# Homotopy Type Theory Seifert-van Kampen theorem (changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

## 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