[[!redirects 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 [[nlab: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 * [agda formalisation](https://github.com/HoTT/HoTT-Agda/tree/e48a16bcd719e2fcb409d79e3f7df6c6b81223bb/theorems/homotopy/vankampen) * [lean formalisation](https://github.com/leanprover/lean2/blob/master/hott/homotopy/vankampen.hlean) ## References * [[HoTT book]] category: homotopy theory