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 componentPlanetmathPlanetmathPlanetmath of A. We state this in type theoryPlanetmathPlanetmath by saying that we have a type S and a function k:SA which is surjectivePlanetmathPlanetmath, i.e. (-1)-connected. If SA and k is the identity function, then we will recover the naive van Kampen theoremMathworldPlanetmath. Another example to keep in mind is when A is pointed and (0-)connected, with k:𝟏A the point: by \autorefthm:minusoneconn-surjective,\autorefthm:connected-pointed this map is surjective just when A is 0-connected.

Let A,B,C,f,g,P,i,j,h be as in the previous sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. We now define, given our surjective map k:SA, an auxiliary type which improves the connectedness of k. Let T be the higher inductive type generated by

  • A function :ST, and

  • For each s,s:S, a function m:(ks=Aks)(s=Ts).

There is an obvious induced function k¯:TA such that k¯=k, and any p:ks=ks is equal to the composite ks=k¯s=k¯mpk¯s=ks.

Lemma 8.7.1.

k¯ is 0-connected.


We must show that for all a:A, the 0-truncation of the type (t:T)(k¯t=a) is contractibleMathworldPlanetmath. 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 |(s,q)|0 where q is the equality k¯s=ks.

It remains to show that for any ϕ:(t:T)(k¯t=ks)0 we have ϕ=|(s,q)|0. Since the latter is a mere proposition, and in particular a set, we may assume that ϕ=|(t,p)|0 for t:T and p:k¯t=ks.

Now we can do inductionMathworldPlanetmath on t:T. If ts, then ks=k¯s=𝑝ks yields via m an equality s=s. Hence by definition of k¯ and of equality in homotopy fibers, we obtain an equality (ks,p)=(ks,q), and thus |(ks,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 (t:T)(k¯t=ks)0), and hence this is automatic. ∎

Remark 8.7.2.

T can be regarded as the (homotopyMathworldPlanetmathPlanetmath) coequalizerMathworldPlanetmath of the “kernel pair” of k. If S and A were sets, then the (-1)-connectivity of k would imply that A is the 0-truncation of this coequalizer (see \autorefcha:set-math). For general types, higher topos theory suggests that (-1)-connectivity of k will imply instead that A is the colimitMathworldPlanetmath (a.k.a. “geometric realization”) of the “simplicial kernel” of k. The type T is the colimit of the “1-skeleton” of this simplicial kernel, so it makes sense that it improves the connectivity of k by 1. More generally, we might expect the colimit of the n-skeletonPlanetmathPlanetmath to improve connectivity by n.

Now we define 𝖼𝗈𝖽𝖾:PP𝒰 by double induction as follows

  • 𝖼𝗈𝖽𝖾(ib,ib) is now a set-quotient of the type of sequencesPlanetmathPlanetmath



    • n:,

    • xk:S and yk:S for 0<kn,

    • p0:Π1B(b,fkx1) and pn:Π1B(fkyn,b) for n>0, and p0:Π1B(b,b) for n=0,

    • pk:Π1B(fkyk,fkxk+1) for 1k<n,

    • qk:Π1C(gkxk,gkyk) for 1kn.

    The quotient is generated by the following equalities (see \autorefrmk:naive):

    (,qk,yk,𝗋𝖾𝖿𝗅fyk,yk,qk+1,) =(,qk\centerdotqk+1,)
    (,pk,xk,𝗋𝖾𝖿𝗅gxk,xk,pk+1,) =(,pk\centerdotpk+1,)
    (,pk-1\centerdotfw,xk,qk,) =(,pk-1,xk,gw\centerdotqk,) (for $w:\Pi_{1}A(kx_{k},kx_{k}^{\prime})$)
    (,qk\centerdotgw,yk,pk,) =(,qk,yk,fw\centerdotpk,). (for $w:\Pi_{1}A(ky_{k},ky_{k}^{\prime})$)

    We will need below the definition of the case of 𝖽𝖾𝖼𝗈𝖽𝖾 on such a sequence, which as before concatenates all the paths pk and qk together with instances of h to give an element of Π1P(ifb,ifb), cf. (LABEL:eq:decode). As before, the other three point cases are nearly identical.

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

    𝖼𝗈𝖽𝖾(ib,ifa)𝖼𝗈𝖽𝖾(ib,jga). (8.7.3)

    Since 𝖼𝗈𝖽𝖾 is set-valued, by \autorefthm:kbar we may assume that a=k¯t for some t:T. Next, we can do induction on t. If ts for s:S, then we define (8.7.3) as in \autorefsec:naive-vankampen:

    (,yn,pn,fks) (,yn,pn,s,𝗋𝖾𝖿𝗅gks,gks),
    (,xn,pn,s,𝗋𝖾𝖿𝗅fks,fks) \mapsfrom(,xn,pn,gks).

    These respect the equivalence relationsMathworldPlanetmath, and define quasi-inversesPlanetmathPlanetmath just as before. Now suppose t varies along ms,s(w) for some w:ks=ks; we must show that (8.7.3) respects transporting along k¯mw. By definition of 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


    is mapped by (8.7.3) to


    But this follows directly from the new generatorsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath we have imposed on the set-quotient relationMathworldPlanetmathPlanetmath defining 𝖼𝗈𝖽𝖾.

  • The other three requisite equivalences are defined similarly.

  • Finally, since the commutativity (LABEL:eq:bfa-bga-comm) is a mere proposition, by (-1)-connectedness of k we may assume that a=ks and a=ks, in which case it follows exactly as before.

Theorem 8.7.4 (van Kampen with a set of basepoints).

For all u,v:P there is an equivalence


with code defined as in this section.


Basically just like before. To show that 𝖽𝖾𝖼𝗈𝖽𝖾 respects the new generators of the quotient relation, we use the naturality of h. And to show that 𝖽𝖾𝖼𝗈𝖽𝖾 respects the equivalences such as (8.7.3), we need to induct on 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 𝖾𝗇𝖼𝗈𝖽𝖾𝖽𝖾𝖼𝗈𝖽𝖾, since the goal is to prove an equality in a set, and so the case of h is trivial. ∎


thm:van-Kampen allows us to calculate the fundamental groupMathworldPlanetmathPlanetmath of a space A, even when A is not a set, provided S is a set, for in that case, each 𝖼𝗈𝖽𝖾(u,v) is, by definition, a set-quotient of a set by a relation. In that respect, it is an improvement over \autorefthm:naive-van-kampen.

Example 8.7.5.

Suppose S:1, so that A has a basepoint a:k() and is connected. Then code for loops in the pushout can be identified with alternating sequences of loops in π1(B,f(a)) and π1(C,g(a)), modulo an equivalence relation which allows us to slide elements of π1(A,a) between them (after applying f and g respectively). Thus, π1(P) can be identified with the amalgamated free product π1(B)*π1(A)π1(C) (the pushout in the category of groups), as constructed in \autorefsec:free-algebras. This (in the case when B and C are open subspaces of P and A their intersectionMathworldPlanetmathPlanetmath) 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:1, so that P is the cofiber B/A. Then every loop in C is equal to reflexivityMathworldPlanetmath, 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 π1(A) is the identityPlanetmathPlanetmathPlanetmath. We can thus identify π1(B/A) with the quotient of the group π1(B) by the normal subgroup generated by the image of π1(A).

Example 8.7.7.

As a further special case of \autorefeg:cofiber, let B:S1S1, let A:S1, and let f:AB pick out the composite loop p\centerdotq\centerdotp-1\centerdotq-1, where p and q are the generating loops in the two copies of S1 comprising B. Then P is a presentationMathworldPlanetmath of the torus T2. Indeed, it is not hard to identify P with the presentation of T2 as described in \autorefsec:hubs-spokes, using the cone on a particular loop. Thus, π1(T2) is the quotient of the free groupMathworldPlanetmath on two generators (i.e., π1(B)) by the relation p\centerdotq\centerdotp-1\centerdotq-1=1. This clearly yields the free abelianMathworldPlanetmath group on two generators, which is Z×Z.

Example 8.7.8.

More generally, any CW complex can be obtained by repeatedly “coning off” spheres, as described in \autorefsec:hubs-spokes. That is, we start with a set X0 of points (“0-cells”), which is the “0-skeleton” of the CW complex. We take the pushout

\xymatrix S_1 ×𝕊^0\ar[r]^-f_1\ar[d] & X_0\ar[d]
1 \ar[r] & X_1 

for some set S1 of 1-cells and some family f1 of “attaching maps”, obtaining the “1-skeleton” X1. Then we take the pushout

\xymatrix S_2 ×𝕊^1\ar[r]^f_2\ar[d] & X_1\ar[d]
1 \ar[r] & X_2 

for some set S2 of 2-cells and some family f2 of attaching maps, obtaining the 2-skeleton X2, 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 1-skeleton, and relations derived from S2 and f2. The pushouts after this stage do not alter the fundamental group, since π1(Sn) is trivial for n>1 (see \autorefsec:pik-le-n).

Example 8.7.9.

In particular, suppose given any presentation of a (set-)group G=XR, with X a set of generators and R a set of words in these generators. Let B:XS1 and A:RS1, with f:AB sending each copy of S1 to the corresponding word in the generating loops of B. It follows that π1(P)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 1-truncate such a type, we obtain a type whose only nontrivial homotopy groupMathworldPlanetmath is G; this is called an Eilenberg–Mac Lane space K(G,1).

Title 8.7.2 The van Kampen theorem with a set of basepoints