8.7.1 Naive van Kampen

We begin with a “naive” version of the van Kampen theorem, which is useful but not quite as useful as the classical version. In sec:better-vankampen we will improve it to a more useful version.

Given types $A,B,C$ and functions $f:A\to B$ and $g:A\to C$, let $P$ be their pushout $B{\bigsqcup }^{A}C$. As we saw in sec:colimits, $P$ is the higher inductive type generated by

• $i:B\to P$,

• $j:C\to P$, and

• for all $x:A$, a path $kx:ifx=jgx$.

Define $\mathrm{𝖼𝗈𝖽𝖾}:P\to P\to 𝒰$ by double induction on $P$ as follows.

• $\mathrm{𝖼𝗈𝖽𝖾}(ib,i{b}^{\prime })$ is a set-quotient (see sec:set-quotients) of the type of sequences

  $$(b,p_0,x_1,q_1,y_1,p_1,x_2,q_2,y_2,p_2,\mathrm{\dots },y_n,p_n,b^{\prime })$$

  where

  • $n:\mathbb{N}$

  • $x_k:A$ and $y_k:A$ for

  • $p_0:{\mathrm{\Pi }}_{1}B(b,f{x}_1)$ and $p_n:{\mathrm{\Pi }}_{1}B(f{y}_n,b^{\prime })$ for $n>0$, and $p_0:{\mathrm{\Pi }}_{1}B(b,b^{\prime })$ for $n=0$

  • $p_k:{\mathrm{\Pi }}_{1}B(f{y}_k,f{x}_{k+1})$ for

  • $q_k:{\mathrm{\Pi }}_{1}C(g{x}_k,g{y}_k)$ for $1\le k\le n$

  The quotient is generated by the following equalities:

  $(\mathrm{\dots },q_k,y_k,{\mathrm{𝗋𝖾𝖿𝗅}}_{f{y}_k},y_k,q_{k+1},\mathrm{\dots })$ $=(\mathrm{\dots },q_k{q}_{k+1},\mathrm{\dots })$

  $(\mathrm{\dots },p_k,x_k,{\mathrm{𝗋𝖾𝖿𝗅}}_{g{x}_k},x_k,p_{k+1},\mathrm{\dots })$ $=(\mathrm{\dots },p_k{p}_{k+1},\mathrm{\dots })$

  (see rmk:naive below). We leave it to the reader to define this type of sequences precisely as an inductive type.

• $\mathrm{𝖼𝗈𝖽𝖾}(jc,j{c}^{\prime })$ is identical, with the roles of $B$ and $C$ reversed. We likewise notationally reverse the roles of $x$ and $y$, and of $p$ and $q$.

• $\mathrm{𝖼𝗈𝖽𝖾}(ib,jc)$ and $\mathrm{𝖼𝗈𝖽𝖾}(jc,ib)$ are similar, with the parity changed so that they start in one type and end in the other.

• For $a:A$ and $b:B$, we require an equivalence

  $$\mathrm{𝖼𝗈𝖽𝖾}(ib,ifa)\simeq \mathrm{𝖼𝗈𝖽𝖾}(ib,jga).$$ (8.7.1)

  We define this to consist of the two functions defined on sequences by

  $(\mathrm{\dots },y_n,p_n,fa)$ $\mapsto (\mathrm{\dots },y_n,p_n,a,{\mathrm{𝗋𝖾𝖿𝗅}}_{ga},ga),$

  $(\mathrm{\dots },x_n,p_n,a,{\mathrm{𝗋𝖾𝖿𝗅}}_{fa},fa)$ $(\mathrm{\dots },x_n,p_n,ga).$

  Both of these functions are easily seen to respect the equivalence relations, and hence to define functions on the types of codes. The left-to-right-to-left composite is

  $$(\mathrm{\dots },y_n,p_n,fa)\mapsto (\mathrm{\dots },y_n,p_n,a,{\mathrm{𝗋𝖾𝖿𝗅}}_{ga},a,{\mathrm{𝗋𝖾𝖿𝗅}}_{fa},fa)$$

  which is equal to the identity by a generating equality of the quotient. The other composite is analogous. Thus we have defined an equivalence (8.7.1).

• Similarly, we require equivalences

  $\mathrm{𝖼𝗈𝖽𝖾}(jc,ifa)$ $\simeq \mathrm{𝖼𝗈𝖽𝖾}(jc,jga)$

  $\mathrm{𝖼𝗈𝖽𝖾}(ifa,ib)$ $\simeq (jga,ib)$

  $\mathrm{𝖼𝗈𝖽𝖾}(ifa,jc)$ $\simeq (jga,jc)$

  all of which are defined in exactly the same way (the second two by adding reflexivity terms on the beginning rather than the end).

• Finally, we need to know that for $a,a^{\prime }:A$, the following diagram commutes:

  $\mathrm{𝖼𝗈𝖽𝖾}$ (ifa,ifa’) [r][d] & $\mathrm{𝖼𝗈𝖽𝖾}$ (ifa,jga’)[d]
  $\mathrm{𝖼𝗈𝖽𝖾}$ (jga,ifa’)[r] & $\mathrm{𝖼𝗈𝖽𝖾}$ (jga,jga’) (8.7.2)

  This amounts to saying that if we add something to the beginning and then something to the end of a sequence, we might as well have done it in the other order.

Remark 8.7.3.

One might expect to see in the definition of $\mathrm{code}$ some additional generating equations for the set-quotient, such as

$(\mathrm{\dots },p_{k-1}fw,x_k^{\prime },q_k,\mathrm{\dots })$ $=(\mathrm{\dots },p_{k-1},x_k,gw{q}_k,\mathrm{\dots })$ (for $w:\Pi_{1}A(x_{k},x_{k}^{\prime})$)

$(\mathrm{\dots },q_{k}gw,y_k^{\prime },p_k,\mathrm{\dots })$ $=(\mathrm{\dots },q_k,y_k,fw{p}_k,\mathrm{\dots }).$ (for $w:\Pi_{1}A(y_{k},y_{k}^{\prime})$)

However, these are not necessary! In fact, they follow automatically by path induction on $w$. This is the main difference between the “naive” van Kampen theorem and the more refined one we will consider in the next subsection.

Continuing on, we can characterize transporting in the fibration $\mathrm{𝖼𝗈𝖽𝖾}$:

• For $p:b{=}_B{b}^{\prime }$ and $u:P$, we have

  $${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{b\mapsto \mathrm{𝖼𝗈𝖽𝖾}(u,ib)}(p,(\mathrm{\dots },y_n,p_n,b))=(\mathrm{\dots },y_n,p_{n}p,b^{\prime }).$$

• For $q:c{=}_C{c}^{\prime }$ and $u:P$, we have

  $${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{c\mapsto \mathrm{𝖼𝗈𝖽𝖾}(u,jc)}(q,(\mathrm{\dots },x_n,q_n,c))=(\mathrm{\dots },x_n,q_{n}q,c^{\prime }).$$

Here we are abusing notation by using the same name for a path in $X$ and its image in ${\mathrm{\Pi }}_{1}X$. Note that transport in ${\mathrm{\Pi }}_{1}X$ is also given by concatenation with (the image of) a path. From this we can prove the above statements by induction on $u$. We also have:

• For $a:A$ and $u:P$,

  $${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{v\mapsto \mathrm{𝖼𝗈𝖽𝖾}(u,v)}(ha,(\mathrm{\dots },y_n,p_n,fa))=(\mathrm{\dots },y_n,p_n,a,{\mathrm{𝗋𝖾𝖿𝗅}}_{ga},ga).$$

This follows essentially from the definition of $\mathrm{𝖼𝗈𝖽𝖾}$.

We also construct a function

$$r:\prod _{u:P}\mathrm{𝖼𝗈𝖽𝖾}(u,u)$$

by induction on $u$ as follows:

$rib$ $:\equiv (b,{\mathrm{𝗋𝖾𝖿𝗅}}_b,b)$

$rjc$ $:\equiv (c,{\mathrm{𝗋𝖾𝖿𝗅}}_c,c)$

and for $rka$ we take the composite equality

${(ka,ka)}_{*}(fa,{\mathrm{𝗋𝖾𝖿𝗅}}_{fa},fa)$ $=(ga,{\mathrm{𝗋𝖾𝖿𝗅}}_{ga},a,{\mathrm{𝗋𝖾𝖿𝗅}}_{fa},a,{\mathrm{𝗋𝖾𝖿𝗅}}_{ga},ga)$

$=(ga,{\mathrm{𝗋𝖾𝖿𝗅}}_{ga},ga)$

where the first equality is by the observation above about transporting in $\mathrm{𝖼𝗈𝖽𝖾}$, and the second is an instance of the set quotient relation used to define $\mathrm{𝖼𝗈𝖽𝖾}$.

We will now prove:

Theorem 8.7.4 (Naive van Kampen theorem).

For all $u\mathrm{,}v\mathrm{:}P$ there is an equivalence

$${\mathrm{\Pi }}_{1}P(u,v)\simeq \mathrm{𝖼𝗈𝖽𝖾}(u,v).$$

Proof.

To define a function

$$\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}:{\mathrm{\Pi }}_{1}P(u,v)\to \mathrm{𝖼𝗈𝖽𝖾}(u,v)$$

it suffices to define a function $(u{=}_{P}v)\to \mathrm{𝖼𝗈𝖽𝖾}(u,v)$, since $\mathrm{𝖼𝗈𝖽𝖾}(u,v)$ is a set. We do this by transport:

$$\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}(p):\equiv {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{v\mapsto \mathrm{𝖼𝗈𝖽𝖾}(u,v)}(p,r(u)).$$

Now to define

$$\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}:\mathrm{𝖼𝗈𝖽𝖾}(u,v)\to {\mathrm{\Pi }}_{1}P(u,v)$$

we proceed as usual by induction on $u,v:P$. In each case for $u$ and $v$, we apply $i$ or $j$ to all the equalities $p_k$ and $q_k$ as appropriate and concatenate the results in $P$, using $h$ to identify the endpoints. For instance, when $u\equiv ib$ and $v\equiv i{b}^{\prime }$, we define

$$\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(b,p_0,x_1,q_1,y_1,p_1,\mathrm{\dots },y_n,p_n,b^{\prime }):\equiv (p_0)h(x_1)j(q_1)h{(y_1)}^{-1}i(p_1)\mathrm{\cdots }h{(y_n)}^{-1}i(p_n).$$ (8.7.5)

This respects the set-quotient equivalence relation and the equivalences such as (8.7.1), since $h:fi\sim gj$ is natural and $f$ and $g$ are functorial.

As usual, to show that the composite

$${\mathrm{\Pi }}_{1}P(u,v)\stackrel{𝖾𝗇𝖼𝗈𝖽𝖾}{\to }\mathrm{𝖼𝗈𝖽𝖾}(u,v)\stackrel{𝖽𝖾𝖼𝗈𝖽𝖾}{\to }{\mathrm{\Pi }}_{1}P(u,v)$$

is the identity, we first peel off the 0-truncation (since the codomain is a set) and then apply path induction. The input ${\mathrm{𝗋𝖾𝖿𝗅}}_u$ goes to $ru$, which then goes back to ${\mathrm{𝗋𝖾𝖿𝗅}}_u$ (applying a further induction on $u$ to decompose $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(ru)$).

Finally, consider the composite

$$\mathrm{𝖼𝗈𝖽𝖾}(u,v)\stackrel{𝖽𝖾𝖼𝗈𝖽𝖾}{\to }{\mathrm{\Pi }}_{1}P(u,v)\stackrel{𝖾𝗇𝖼𝗈𝖽𝖾}{\to }\mathrm{𝖼𝗈𝖽𝖾}(u,v).$$

We proceed by induction on $u,v:P$. When $u\equiv ib$ and $v\equiv i{b}^{\prime }$, this composite is

i.e., the identity function. (To be precise, there is an implicit inductive argument needed here.) The other three point cases are analogous, and the path cases are trivial since all the types are sets. ∎

thm:naive-van-kampen allows us to calculate the fundamental groups of many types, provided $A$ is a set, for in that case, each $\mathrm{𝖼𝗈𝖽𝖾}(u,v)$ is, by definition, a set-quotient of a set by a relation.

Example 8.7.5.

Let $A\mathrm{:}\mathrm{\equiv }\mathrm{2}$, $B\mathrm{:}\mathrm{\equiv }\mathrm{1}$, and $C\mathrm{:}\mathrm{\equiv }\mathrm{1}$. Then $P\mathrm{\simeq }{S}^{\mathrm{1}}$. Inspecting the definition of, say, $\mathrm{code}\mathit{}\mathrm{(}i\mathit{}\mathrm{(}\mathrm{\star }\mathrm{)}\mathrm{,}i\mathit{}\mathrm{(}\mathrm{\star }\mathrm{)}\mathrm{)}$, we see that the paths all may as well be trivial, so the only information is in the sequence of elements $x_{\mathrm{1}}\mathrm{,}{y}_{\mathrm{1}}\mathrm{,}\mathrm{\dots }\mathrm{,}{x}_n\mathrm{,}{y}_n\mathrm{:}\mathrm{2}$. Moreover, if we have $x_k\mathrm{=}{y}_k$ or $y_k\mathrm{=}{x}_{k\mathrm{+}\mathrm{1}}$ for any $k$, then the set-quotient relations allow us to excise both of those elements. Thus, every such sequence is equal to a canonical reduced one in which no two adjacent elements are equal. Clearly such a reduced sequence is uniquely determined by its length (a natural number $n$) together with, if $n\mathrm{>}\mathrm{1}$, the information of whether $x_{\mathrm{1}}$ is ${\mathrm{0}}_{\mathrm{2}}$ or ${\mathrm{1}}_{\mathrm{2}}$, since that determines the rest of the sequence uniquely. And these data can, of course, be identified with an integer, where $n$ is the absolute value and $x_{\mathrm{1}}$ encodes the sign. Thus we recover ${\pi }_{\mathrm{1}}\mathit{}\mathrm{(}{S}^{\mathrm{1}}\mathrm{)}\mathrm{\cong }\mathrm{Z}$.

Since thm:naive-van-kampen asserts only a bijection of families of sets, this isomorphism ${\pi }_1(S^1)\cong \mathbb{Z}$ is likewise only a bijection of sets. We could, however, define a concatenation operation on $\mathrm{𝖼𝗈𝖽𝖾}$ (by concatenating sequences) and show that $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}$ and $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}$ form an isomorphism respecting this structure. (In the language of cha:category-theory, these would be “pregroupoids”.) We leave the details to the reader.

Example 8.7.6.

More generally, let $B\mathrm{:}\mathrm{\equiv }\mathrm{1}$ and $C\mathrm{:}\mathrm{\equiv }\mathrm{1}$ but $A$ be arbitrary, so that $P$ is the suspension of $A$. Then once again the paths $p_k$ and $q_k$ are trivial, so that the only information in a path code is a sequence of elements $x_{\mathrm{1}}\mathrm{,}{y}_{\mathrm{1}}\mathrm{,}\mathrm{\dots }\mathrm{,}{x}_n\mathrm{,}{y}_n\mathrm{:}A$. The first two generating equalities say that adjacent equal elements can be canceled, so it makes sense to think of this sequence as a word of the form

$$x_1{y}_1^{-1}{x}_2{y}_2^{-1}\mathrm{\cdots }{x}_n{y}_n^{-1}$$

in a group. Indeed, it looks similar to the free group on $A$ (or equivalently on ${\mathrm{\parallel }A\mathrm{\parallel }}_{\mathrm{0}}$; see thm:freegroup-nonset), but we are considering only words that start with a non-inverted element, alternate between inverted and non-inverted elements, and end with an inverted one. This effectively reduces the size of the generating set by one. For instance, if $A$ has a point $a\mathrm{:}A$, then we can identify ${\pi }_{\mathrm{1}}\mathit{}\mathrm{(}\mathrm{\Sigma }\mathit{}A\mathrm{)}$ with the group presented by ${\mathrm{\parallel }A\mathrm{\parallel }}_{\mathrm{0}}$ as generators with the relation $\mathrm{|}a{\mathrm{|}}_{\mathrm{0}}\mathrm{=}e$; see ex:vksusppt,ex:vksuspnopt for details.

Example 8.7.7.

Let $A\mathrm{:}\mathrm{\equiv }\mathrm{1}$ and $B$ and $C$ be arbitrary, so that $f$ and $g$ simply equip $B$ and $C$ with basepoints $b$ and $c$, say. Then $P$ is the wedge $B\mathrm{\vee }C$ of $B$ and $C$ (the coproduct in the category of based spaces). In this case, it is the elements $x_k$ and $y_k$ which are trivial, so that the only information is a sequence of loops $\mathrm{(}{p}_{\mathrm{0}}\mathrm{,}{q}_{\mathrm{1}}\mathrm{,}{p}_{\mathrm{1}}\mathrm{,}\mathrm{\dots }\mathrm{,}{p}_n\mathrm{)}$ with $p_k\mathrm{:}{\pi }_{\mathrm{1}}\mathit{}\mathrm{(}B\mathrm{,}b\mathrm{)}$ and $q_k\mathrm{:}{\pi }_{\mathrm{1}}\mathit{}\mathrm{(}C\mathrm{,}c\mathrm{)}$. Such sequences, modulo the equivalence relation we have imposed, are easily identified with the explicit description of the free product of the groups ${\pi }_{\mathrm{1}}\mathit{}\mathrm{(}B\mathrm{,}b\mathrm{)}$ and ${\pi }_{\mathrm{1}}\mathit{}\mathrm{(}C\mathrm{,}c\mathrm{)}$, as constructed in sec:free-algebras. Thus, we have ${\pi }_{\mathrm{1}}\mathit{}\mathrm{(}B\mathrm{\vee }C\mathrm{)}\mathrm{\cong }{\pi }_{\mathrm{1}}\mathit{}\mathrm{(}B\mathrm{)}\mathrm{*}{\pi }_{\mathrm{1}}\mathit{}\mathrm{(}C\mathrm{)}$.

However, thm:naive-van-kampen stops just short of being the full classical van Kampen theorem, which handles the case where $A$ is not necessarily a set, and states that ${\pi }_1(B{\bigsqcup }^{A}C)\cong {\pi }_1(B){*}_{{\pi }_1(A)}{\pi }_1(C)$ (with base point coming from $A$). Indeed, the conclusion of thm:naive-van-kampen says nothing at all about ${\pi }_1(A)$; the paths in $A$ are “built into the quotienting” in a type-theoretic way that makes it hard to extract explicit information, in that $\mathrm{𝖼𝗈𝖽𝖾}(u,v)$ is a set-quotient of a non-set by a relation. For this reason, in the next subsection we consider a better version of the van Kampen theorem.

Title	8.7.1 Naive van Kampen