8.7.2 The van Kampen theorem with a set of basepoints
The improvement of van Kampen we present now is closely analogous to a similar improvement in classical algebraic topology, where $A$ is equipped with a set $S$ of base points. In fact, it turns out to be unnecessary for our proof to assume that the “set of basepoints” is a set — it might just as well be an arbitrary type; the utility of assuming $S$ is a set arises later, when applying the theorem to obtain computations. What is important is that $S$ contains at least one point in each connected component^{} of $A$. We state this in type theory^{} by saying that we have a type $S$ and a function $k:S\to A$ which is surjective^{}, i.e. $(1)$connected. If $S\equiv A$ and $k$ is the identity function, then we will recover the naive van Kampen theorem^{}. Another example to keep in mind is when $A$ is pointed and (0)connected, with $k:\mathrm{\U0001d7cf}\to A$ the point: by \autorefthm:minusoneconnsurjective,\autorefthm:connectedpointed this map is surjective just when $A$ is 0connected.
Let $A,B,C,f,g,P,i,j,h$ be as in the previous section^{}. We now define, given our surjective map $k:S\to A$, an auxiliary type which improves the connectedness of $k$. Let $T$ be the higher inductive type generated by

•
A function $\mathrm{\ell}:S\to T$, and

•
For each $s,{s}^{\prime}:S$, a function $m:(ks{=}_{A}k{s}^{\prime})\to (\mathrm{\ell}s{=}_{T}\mathrm{\ell}{s}^{\prime})$.
There is an obvious induced function $\overline{k}:T\to A$ such that $\overline{k}\mathrm{\ell}=k$, and any $p:ks=k{s}^{\prime}$ is equal to the composite $ks=\overline{k}\mathrm{\ell}s\stackrel{\overline{k}mp}{=}\overline{k}\mathrm{\ell}{s}^{\prime}=k{s}^{\prime}$.
Lemma 8.7.1.
$\overline{k}$ is 0connected.
Proof.
We must show that for all $a:A$, the 0truncation of the type ${\sum}_{(t:T)}(\overline{k}t=a)$ is contractible^{}. Since contractibility is a mere proposition and $k$ is $(1)$connected, we may assume that $a=ks$ for some $s:S$. Now we can take the center of contraction to be ${\left(\mathrm{\ell}s,q)\right}_{0}$ where $q$ is the equality $\overline{k}\mathrm{\ell}s=ks$.
It remains to show that for any $\varphi :\parallel {\sum}_{(t:T)}(\overline{k}t=ks){\parallel}_{0}$ we have $\varphi =(\mathrm{\ell}s,q){}_{0}$. Since the latter is a mere proposition, and in particular a set, we may assume that $\varphi =(t,p){}_{0}$ for $t:T$ and $p:\overline{k}t=ks$.
Now we can do induction^{} on $t:T$. If $t\equiv \mathrm{\ell}{s}^{\prime}$, then $k{s}^{\prime}=\overline{k}\mathrm{\ell}{s}^{\prime}\stackrel{\mathit{p}}{=}ks$ yields via $m$ an equality $\mathrm{\ell}s=\mathrm{\ell}{s}^{\prime}$. Hence by definition of $\overline{k}$ and of equality in homotopy fibers, we obtain an equality $(k{s}^{\prime},p)=(ks,q)$, and thus $(k{s}^{\prime},p){}_{0}=(ks,q){}_{0}$. Next we must show that as $t$ varies along $m$ these equalities agree. But they are equalities in a set (namely $\parallel {\sum}_{(t:T)}(\overline{k}t=ks){\parallel}_{0}$), and hence this is automatic. ∎
Remark 8.7.2.
$T$ can be regarded as the (homotopy^{}) coequalizer^{} of the “kernel pair” of $k$. If $S$ and $A$ were sets, then the $\mathrm{(}\mathrm{}\mathrm{1}\mathrm{)}$connectivity of $k$ would imply that $A$ is the $\mathrm{0}$truncation of this coequalizer (see \autorefcha:setmath). For general types, higher topos theory suggests that $\mathrm{(}\mathrm{}\mathrm{1}\mathrm{)}$connectivity of $k$ will imply instead that $A$ is the colimit^{} (a.k.a. “geometric realization”) of the “simplicial kernel” of $k$. The type $T$ is the colimit of the “1skeleton” of this simplicial kernel, so it makes sense that it improves the connectivity of $k$ by $\mathrm{1}$. More generally, we might expect the colimit of the $n$skeleton^{} to improve connectivity by $n$.
Now we define $\mathrm{\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}:P\to P\to \mathcal{U}$ by double induction as follows

•
$\mathrm{\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}(ib,i{b}^{\prime})$ is now a setquotient 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}:S$ and ${y}_{k}:S$ for $$,

–
${p}_{0}:{\mathrm{\Pi}}_{1}B(b,fk{x}_{1})$ and ${p}_{n}:{\mathrm{\Pi}}_{1}B(fk{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(fk{y}_{k},fk{x}_{k+1})$ for $$,

–
${q}_{k}:{\mathrm{\Pi}}_{1}C(gk{x}_{k},gk{y}_{k})$ for $1\le k\le n$.
The quotient is generated by the following equalities (see \autorefrmk:naive):
$(\mathrm{\dots},{q}_{k},{y}_{k},{\mathrm{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{f{y}_{k}},{y}_{k},{q}_{k+1},\mathrm{\dots})$ $=(\mathrm{\dots},{q}_{k}\text{centerdot}{q}_{k+1},\mathrm{\dots})$ $(\mathrm{\dots},{p}_{k},{x}_{k},{\mathrm{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{g{x}_{k}},{x}_{k},{p}_{k+1},\mathrm{\dots})$ $=(\mathrm{\dots},{p}_{k}\text{centerdot}{p}_{k+1},\mathrm{\dots})$ $(\mathrm{\dots},{p}_{k1}\text{centerdot}fw,{x}_{k}^{\prime},{q}_{k},\mathrm{\dots})$ $=(\mathrm{\dots},{p}_{k1},{x}_{k},gw\text{centerdot}{q}_{k},\mathrm{\dots})$ (for $w:\Pi_{1}A(kx_{k},kx_{k}^{\prime})$) $(\mathrm{\dots},{q}_{k}\text{centerdot}gw,{y}_{k}^{\prime},{p}_{k},\mathrm{\dots})$ $=(\mathrm{\dots},{q}_{k},{y}_{k},fw\text{centerdot}{p}_{k},\mathrm{\dots}).$ (for $w:\Pi_{1}A(ky_{k},ky_{k}^{\prime})$) We will need below the definition of the case of $\mathrm{\U0001d5bd\U0001d5be\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}$ on such a sequence, which as before concatenates all the paths ${p}_{k}$ and ${q}_{k}$ together with instances of $h$ to give an element of ${\mathrm{\Pi}}_{1}P(ifb,if{b}^{\prime})$, cf. (LABEL:eq:decode). As before, the other three point cases are nearly identical.

–

•
For $a:A$ and $b:B$, we require an equivalence
$$\mathrm{\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}(ib,ifa)\simeq \mathrm{\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}(ib,jga).$$ (8.7.3) Since $\mathrm{\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}$ is setvalued, by \autorefthm:kbar we may assume that $a=\overline{k}t$ for some $t:T$. Next, we can do induction on $t$. If $t\equiv \mathrm{\ell}s$ for $s:S$, then we define (8.7.3) as in \autorefsec:naivevankampen:
$(\mathrm{\dots},{y}_{n},{p}_{n},fks)$ $\mapsto (\mathrm{\dots},{y}_{n},{p}_{n},s,{\mathrm{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{gks},gks),$ $(\mathrm{\dots},{x}_{n},{p}_{n},s,{\mathrm{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{fks},fks)$ $\text{mapsfrom}(\mathrm{\dots},{x}_{n},{p}_{n},gks).$ These respect the equivalence relations^{}, and define quasiinverses^{} just as before. Now suppose $t$ varies along ${m}_{s,{s}^{\prime}}(w)$ for some $w:ks=k{s}^{\prime}$; we must show that (8.7.3) respects transporting along $\overline{k}mw$. By definition of $\overline{k}$, this essentially boils down to transporting along $w$ itself. By the characterization of transport in path types, what we need to show is that
$${w}_{*}(\mathrm{\dots},{y}_{n},{p}_{n},fks)=(\mathrm{\dots},{y}_{n},{p}_{n}\text{centerdot}fw,fk{s}^{\prime})$$ is mapped by (8.7.3) to
$${w}_{*}(\mathrm{\dots},{y}_{n},{p}_{n},s,{\mathrm{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{gks},gks)=(\mathrm{\dots},{y}_{n},{p}_{n},s,{\mathrm{\U0001d5cb\U0001d5be\U0001d5bf\U0001d5c5}}_{gks}\text{centerdot}gw,gk{s}^{\prime})$$ But this follows directly from the new generators^{} we have imposed on the setquotient relation^{} defining $\mathrm{\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}$.

•
The other three requisite equivalences are defined similarly.

•
Finally, since the commutativity (LABEL:eq:bfabgacomm) is a mere proposition, by $(1)$connectedness of $k$ we may assume that $a=ks$ and ${a}^{\prime}=k{s}^{\prime}$, in which case it follows exactly as before.
Theorem 8.7.4 (van Kampen with a set of basepoints).
For all $u\mathrm{,}v\mathrm{:}P$ there is an equivalence
$${\mathrm{\Pi}}_{1}P(u,v)\simeq \mathrm{\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}(u,v).$$ 
with $\mathrm{code}$ defined as in this section.
Proof.
Basically just like before. To show that $\mathrm{\U0001d5bd\U0001d5be\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}$ respects the new generators of the quotient relation, we use the naturality of $h$. And to show that $\mathrm{\U0001d5bd\U0001d5be\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}$ respects the equivalences such as (8.7.3), we need to induct on $\overline{k}$ and on $T$ in order to decompose those equivalences into their definitions, but then it becomes again simply functoriality of $f$ and $g$. The rest is easy. In particular, no additional argument is required for $\mathrm{\U0001d5be\U0001d5c7\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}\circ \mathrm{\U0001d5bd\U0001d5be\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}$, since the goal is to prove an equality in a set, and so the case of $h$ is trivial. ∎
thm:vanKampen allows us to calculate the fundamental group^{} of a space $A$, even when $A$ is not a set, provided $S$ is a set, for in that case, each $\mathrm{\U0001d5bc\U0001d5c8\U0001d5bd\U0001d5be}(u,v)$ is, by definition, a setquotient of a set by a relation. In that respect, it is an improvement over \autorefthm:naivevankampen.
Example 8.7.5.
Suppose $S\mathrm{:}\mathrm{\equiv}\mathrm{1}$, so that $A$ has a basepoint $a\mathrm{:}\mathrm{\equiv}k\mathrm{(}\mathrm{\star}\mathrm{)}$ and is connected. Then code for loops in the pushout can be identified with alternating sequences of loops in ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}B\mathrm{,}f\mathit{}\mathrm{(}a\mathrm{)}\mathrm{)}$ and ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}C\mathrm{,}g\mathit{}\mathrm{(}a\mathrm{)}\mathrm{)}$, modulo an equivalence relation which allows us to slide elements of ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}A\mathrm{,}a\mathrm{)}$ between them (after applying $f$ and $g$ respectively). Thus, ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}P\mathrm{)}$ can be identified with the amalgamated free product ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}B\mathrm{)}{\mathrm{*}}_{{\pi}_{\mathrm{1}}\mathit{}\mathrm{(}A\mathrm{)}}{\pi}_{\mathrm{1}}\mathit{}\mathrm{(}C\mathrm{)}$ (the pushout in the category of groups), as constructed in \autorefsec:freealgebras. This (in the case when $B$ and $C$ are open subspaces of $P$ and $A$ their intersection^{}) is probably the most classical version of the van Kampen theorem.
Example 8.7.6.
As a special case of \autorefeg:clvk, suppose additionally that $C\mathrm{:}\mathrm{\equiv}\mathrm{1}$, so that $P$ is the cofiber $B\mathrm{/}A$. Then every loop in $C$ is equal to reflexivity^{}, so the relations on path codes allow us to collapse all sequences to a single loop in $B$. The additional relations require that multiplying on the left, right, or in the middle by an element in the image of ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}A\mathrm{)}$ is the identity^{}. We can thus identify ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}B\mathrm{/}A\mathrm{)}$ with the quotient of the group ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}B\mathrm{)}$ by the normal subgroup generated by the image of ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}A\mathrm{)}$.
Example 8.7.7.
As a further special case of \autorefeg:cofiber, let $B\mathrm{:}\mathrm{\equiv}{S}^{\mathrm{1}}\mathrm{\vee}{S}^{\mathrm{1}}$, let $A\mathrm{:}\mathrm{\equiv}{S}^{\mathrm{1}}$, and let $f\mathrm{:}A\mathrm{\to}B$ pick out the composite loop $p\mathit{}\text{centerdot}\mathit{}q\mathit{}\text{centerdot}\mathit{}{p}^{\mathrm{}\mathrm{1}}\mathit{}\text{centerdot}\mathit{}{q}^{\mathrm{}\mathrm{1}}$, where $p$ and $q$ are the generating loops in the two copies of ${S}^{\mathrm{1}}$ comprising $B$. Then $P$ is a presentation^{} of the torus ${T}^{\mathrm{2}}$. Indeed, it is not hard to identify $P$ with the presentation of ${T}^{\mathrm{2}}$ as described in \autorefsec:hubsspokes, using the cone on a particular loop. Thus, ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}{T}^{\mathrm{2}}\mathrm{)}$ is the quotient of the free group^{} on two generators (i.e., ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}B\mathrm{)}$) by the relation $p\mathit{}\text{centerdot}\mathit{}q\mathit{}\text{centerdot}\mathit{}{p}^{\mathrm{}\mathrm{1}}\mathit{}\text{centerdot}\mathit{}{q}^{\mathrm{}\mathrm{1}}\mathrm{=}\mathrm{1}$. This clearly yields the free abelian^{} group on two generators, which is $\mathrm{Z}\mathrm{\times}\mathrm{Z}$.
Example 8.7.8.
More generally, any CW complex can be obtained by repeatedly “coning off” spheres, as described in \autorefsec:hubsspokes. That is, we start with a set ${X}_{\mathrm{0}}$ of points (“0cells”), which is the “0skeleton” of the CW complex. We take the pushout
$$\text{xymatrixS\_1}\times \text{\mathbb{S}}\mathit{\text{^0}}\text{ar}\mathit{\text{[r]^f\_1}}\text{ar}\mathit{\text{[d] \& X\_0}}\text{ar}\mathit{\text{[d]}}{\text{1ar[r] X\_1}}$$ 
for some set ${S}_{\mathrm{1}}$ of 1cells and some family ${f}_{\mathrm{1}}$ of “attaching maps”, obtaining the “1skeleton” ${X}_{\mathrm{1}}$. Then we take the pushout
$$\text{xymatrixS\_2}\times \text{\mathbb{S}}\mathit{\text{^1}}\text{ar}\mathit{\text{[r]^f\_2}}\text{ar}\mathit{\text{[d] \& X\_1}}\text{ar}\mathit{\text{[d]}}{\text{1ar[r] X\_2}}$$ 
for some set ${S}_{\mathrm{2}}$ of 2cells and some family ${f}_{\mathrm{2}}$ of attaching maps, obtaining the 2skeleton ${X}_{\mathrm{2}}$, and so on. The fundamental group of each pushout can be calculated from the van Kampen theorem: we obtain the group presented by generators derived from the 1skeleton, and relations derived from ${S}_{\mathrm{2}}$ and ${f}_{\mathrm{2}}$. The pushouts after this stage do not alter the fundamental group, since ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}{\mathrm{S}}^{n}\mathrm{)}$ is trivial for $n\mathrm{>}\mathrm{1}$ (see \autorefsec:piklen).
Example 8.7.9.
In particular, suppose given any presentation of a (set)group $G\mathrm{=}\mathrm{\u27e8}X\mathrm{\mid}R\mathrm{\u27e9}$, with $X$ a set of generators and $R$ a set of words in these generators. Let $B\mathrm{:}\mathrm{\equiv}{\mathrm{\bigvee}}_{X}{S}^{\mathrm{1}}$ and $A\mathrm{:}\mathrm{\equiv}{\mathrm{\bigvee}}_{R}{S}^{\mathrm{1}}$, with $f\mathrm{:}A\mathrm{\to}B$ sending each copy of ${S}^{\mathrm{1}}$ to the corresponding word in the generating loops of $B$. It follows that ${\pi}_{\mathrm{1}}\mathit{}\mathrm{(}P\mathrm{)}\mathrm{\cong}G$; thus we have constructed a connected type whose fundamental group is $G$. Since any group has a presentation, any group is the fundamental group of some type. If we 1truncate such a type, we obtain a type whose only nontrivial homotopy group^{} is $G$; this is called an Eilenberg–Mac Lane space $K\mathit{}\mathrm{(}G\mathrm{,}\mathrm{1}\mathrm{)}$.
Title  8.7.2 The van Kampen theorem with a set of basepoints 
\metatable 