The van Kampen theorem calculates the fundamental group of a pushout of spaces. It is traditionally stated for a topological space which is the union of two open subspaces and , but in homotopy-theoretic terms, this is just a a convenient way of ensuring that is the pushout of and over their intersection.
It is useful to generalise the fundamental group of a type to the fundamental groupoid
This has induced groupoid operations coming from the identity type: concatenation, inverses, identity and function application.
Let be types? and and functions?. Let be their pushout.
By defining a special code function the statement of the theorem becomes:
this is the encode-decode method?.
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.
Revision on January 19, 2019 at 19:05:25 by Ali Caglayan. See the history of this page for a list of all contributions to it.