# 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 \autorefsec: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\sqcup^{A}C$. As we saw in \autorefsec: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 $\mathsf{code}:P\to P\to\mathcal{U}$ by double induction on $P$ as follows.

• $\mathsf{code}(ib,ib^{\prime})$ is a set-quotient (see \autorefsec: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},\dots,y_{n},p_{n},b^{% \prime})$

where

• $n:\mathbb{N}$

• $x_{k}:A$ and $y_{k}:A$ for $0

• $p_{0}:\Pi_{1}B(b,fx_{1})$ and $p_{n}:\Pi_{1}B(fy_{n},b^{\prime})$ for $n>0$, and $p_{0}:\Pi_{1}B(b,b^{\prime})$ for $n=0$

• $p_{k}:\Pi_{1}B(fy_{k},fx_{k+1})$ for $1\leq k

• $q_{k}:\Pi_{1}C(gx_{k},gy_{k})$ for $1\leq k\leq n$

The quotient is generated by the following equalities:

 $\displaystyle(\dots,q_{k},y_{k},\mathsf{refl}_{fy_{k}},y_{k},q_{k+1},\dots)$ $\displaystyle=(\dots,q_{k}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}q_{k+1},\dots)$ $\displaystyle(\dots,p_{k},x_{k},\mathsf{refl}_{gx_{k}},x_{k},p_{k+1},\dots)$ $\displaystyle=(\dots,p_{k}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}p_{k+1},\dots)$

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

• $\mathsf{code}(jc,jc^{\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$.

• $\mathsf{code}(ib,jc)$ and $\mathsf{code}(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

 $\mathsf{code}(ib,ifa)\simeq\mathsf{code}(ib,jga).$ (8.7.1)

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

 $\displaystyle(\dots,y_{n},p_{n},fa)$ $\displaystyle\mapsto(\dots,y_{n},p_{n},a,\mathsf{refl}_{ga},ga),$ $\displaystyle(\dots,x_{n},p_{n},a,\mathsf{refl}_{fa},fa)$ $\displaystyle\mapsfrom(\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

 $(\dots,y_{n},p_{n},fa)\mapsto(\dots,y_{n},p_{n},a,\mathsf{refl}_{ga},a,\mathsf% {refl}_{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

 $\displaystyle\mathsf{code}(jc,ifa)$ $\displaystyle\simeq\mathsf{code}(jc,jga)$ $\displaystyle\mathsf{code}(ifa,ib)$ $\displaystyle\simeq(jga,ib)$ $\displaystyle\mathsf{code}(ifa,jc)$ $\displaystyle\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:

 \xymatrix $\mathsf{code}$ (ifa,ifa’) \ar[r]\ar[d] & $\mathsf{code}$ (ifa,jga’)\ar[d] $\mathsf{code}$ (jga,ifa’)\ar[r] & $\mathsf{code}$ (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 $\mathsf{code}$ some additional generating equations for the set-quotient, such as

 $\displaystyle(\dots,p_{k-1}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}fw,x_{k}^{\prime},q_{k},\dots)$ $\displaystyle=(\dots,p_{k-1},x_{k},gw\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}q_{k},\dots){}$ (for $w:\Pi_{1}A(x_{k},x_{k}^{\prime})$) $\displaystyle(\dots,q_{k}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}gw,y_{k}^{\prime},p_{k},\dots)$ $\displaystyle=(\dots,q_{k},y_{k},fw\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}p_{k},\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 $\mathsf{code}$:

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

 $\mathsf{transport}^{b\mapsto\mathsf{code}(u,ib)}(p,(\dots,y_{n},p_{n},b))=(% \dots,y_{n},p_{n}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}p,b^{\prime}).$
• For $q:c=_{C}c^{\prime}$ and $u:P$, we have

 $\mathsf{transport}^{c\mapsto\mathsf{code}(u,jc)}(q,(\dots,x_{n},q_{n},c))=(% \dots,x_{n},q_{n}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}q,c^{\prime}).$

Here we are abusing notation by using the same name for a path in $X$ and its image in $\Pi_{1}X$. Note that transport in $\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$,

 $\mathsf{transport}^{v\mapsto\mathsf{code}(u,v)}(ha,(\dots,y_{n},p_{n},fa))=(% \dots,y_{n},p_{n},a,\mathsf{refl}_{ga},ga).$

This follows essentially from the definition of $\mathsf{code}$.

We also construct a function

 $r:\mathchoice{\prod_{u:P}\,}{\mathchoice{{\textstyle\prod_{(u:P)}}}{\prod_{(u:% P)}}{\prod_{(u:P)}}{\prod_{(u:P)}}}{\mathchoice{{\textstyle\prod_{(u:P)}}}{% \prod_{(u:P)}}{\prod_{(u:P)}}{\prod_{(u:P)}}}{\mathchoice{{\textstyle\prod_{(u% :P)}}}{\prod_{(u:P)}}{\prod_{(u:P)}}{\prod_{(u:P)}}}\mathsf{code}(u,u)$

by induction on $u$ as follows:

 $\displaystyle rib$ $\displaystyle:\!\!\equiv(b,\mathsf{refl}_{b},b)$ $\displaystyle rjc$ $\displaystyle:\!\!\equiv(c,\mathsf{refl}_{c},c)$

and for $rka$ we take the composite equality

 $\displaystyle(ka,ka)_{*}(fa,\mathsf{refl}_{fa},fa)$ $\displaystyle=(ga,\mathsf{refl}_{ga},a,\mathsf{refl}_{fa},a,\mathsf{refl}_{ga}% ,ga)$ $\displaystyle=(ga,\mathsf{refl}_{ga},ga)$

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

We will now prove:

###### Theorem 8.7.4 (Naive van Kampen theorem).

For all $u,v:P$ there is an equivalence

 $\Pi_{1}P(u,v)\simeq\mathsf{code}(u,v).$
###### Proof.

To define a function

 $\mathsf{encode}:\Pi_{1}P(u,v)\to\mathsf{code}(u,v)$

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

 $\mathsf{encode}(p):\!\!\equiv\mathsf{transport}^{v\mapsto\mathsf{code}(u,v)}(p% ,r(u)).$

Now to define

 $\mathsf{decode}:\mathsf{code}(u,v)\to\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 ib^{\prime}$, we define

 $\mathsf{decode}(b,p_{0},x_{1},q_{1},y_{1},p_{1},\dots,y_{n},p_{n},b^{\prime}):% \!\!\equiv(p_{0})\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}h(x_{1})\mathchoice{\mathbin{\raisebox{2.1% 5pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}j(q_{1})\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{h(y_% {1})}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}% {\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}i(p_{1})\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\cdots\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{h(y_% {n})}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}% {\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}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

 $\Pi_{1}P(u,v)\xrightarrow{\mathsf{encode}}\mathsf{code}(u,v)\xrightarrow{% \mathsf{decode}}\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 $\mathsf{refl}_{u}$ goes to $ru$, which then goes back to $\mathsf{refl}_{u}$ (applying a further induction on $u$ to decompose $\mathsf{decode}(ru)$).

Finally, consider the composite

 $\mathsf{code}(u,v)\xrightarrow{\mathsf{decode}}\Pi_{1}P(u,v)\xrightarrow{% \mathsf{encode}}\mathsf{code}(u,v).$

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

 (b,p_{0},x_{1},q_{1},y_{1},p_{1},\dots,y_{n},p_{n},b^{\prime})\begin{aligned} % &\displaystyle\mapsto\Big{(}ip_{0}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}hx_{1}\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}jq_{1}% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathord{{hy_{1}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}ip_{1}\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\cdots% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathord{{hy_{n}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}ip_{n}\Big{)}_{*}(rib)\\ &\displaystyle=(ip_{n})_{*}\cdots(jq_{1})_{*}(hx_{1})_{*}(ip_{0})_{*}(b,% \mathsf{refl}_{b},b)\\ &\displaystyle=(ip_{n})_{*}\cdots(jq_{1})_{*}(hx_{1})_{*}(b,p_{0},ifx_{1})\\ &\displaystyle=(ip_{n})_{*}\cdots(jq_{1})_{*}(b,p_{0},x_{1},\mathsf{refl}_{gx_% {1}},jgx_{1})\\ &\displaystyle=(ip_{n})_{*}\cdots(b,p_{0},x_{1},q_{1},jgy_{1})\\ &\displaystyle=\quad\vdots\\ &\displaystyle=(b,p_{0},x_{1},q_{1},y_{1},p_{1},\dots,y_{n},p_{n},b^{\prime}).% \end{aligned}

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. ∎

\autoref

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

###### Example 8.7.5.

Let $A:\!\!\equiv\mathbf{2}$, $B:\!\!\equiv\mathbf{1}$, and $C:\!\!\equiv\mathbf{1}$. Then $P\simeq S^{1}$. Inspecting the definition of, say, $\mathsf{code}(i(\star),i(\star))$, we see that the paths all may as well be trivial, so the only information is in the sequence of elements $x_{1},y_{1},\dots,x_{n},y_{n}:\mathbf{2}$. Moreover, if we have $x_{k}=y_{k}$ or $y_{k}=x_{k+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>1$, the information of whether $x_{1}$ is ${0_{\mathbf{2}}}$ or ${1_{\mathbf{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_{1}$ encodes the sign. Thus we recover $\pi_{1}(S^{1})\cong\mathbb{Z}$.

Since \autorefthm: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 $\mathsf{code}$ (by concatenating sequences) and show that $\mathsf{encode}$ and $\mathsf{decode}$ form an isomorphism respecting this structure. (In the language of \autorefcha:category-theory, these would be “pregroupoids”.) We leave the details to the reader.

###### Example 8.7.6.

More generally, let $B:\!\!\equiv\mathbf{1}$ and $C:\!\!\equiv\mathbf{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_{1},y_{1},\dots,x_{n},y_{n}: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}\cdots x_{n}y_{n}^{-1}$

in a group. Indeed, it looks similar to the free group on $A$ (or equivalently on $\mathopen{}\left\|A\right\|_{0}\mathclose{}$; see \autorefthm: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:A$, then we can identify $\pi_{1}(\Sigma A)$ with the group presented by $\mathopen{}\left\|A\right\|_{0}\mathclose{}$ as generators with the relation $\mathopen{}\left|a\right|_{0}\mathclose{}=e$; see \autorefex:vksusppt,\autorefex:vksuspnopt for details.

###### Example 8.7.7.

Let $A:\!\!\equiv\mathbf{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\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 $(p_{0},q_{1},p_{1},\dots,p_{n})$ with $p_{k}:\pi_{1}(B,b)$ and $q_{k}:\pi_{1}(C,c)$. Such sequences, modulo the equivalence relation we have imposed, are easily identified with the explicit description of the free product of the groups $\pi_{1}(B,b)$ and $\pi_{1}(C,c)$, as constructed in \autorefsec:free-algebras. Thus, we have $\pi_{1}(B\vee C)\cong\pi_{1}(B)*\pi_{1}(C)$.

However, \autorefthm: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\sqcup^{A}C)\cong\pi_{1}(B)*_{\pi_{1}(A)}\pi_{1}(C)$ (with base point coming from $A$). Indeed, the conclusion of \autorefthm: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 $\mathsf{code}(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
\metatable