8.7.1 Naive van Kampen

We begin with a “naive” version of the van Kampen theoremMathworldPlanetmath, 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:AB and g:AC, let P be their pushout BAC. As we saw in \autorefsec:colimitsMathworldPlanetmath, P is the higher inductive type generated by

  • i:BP,

  • j:CP, and

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

Define 𝖼𝗈𝖽𝖾:PP𝒰 by double inductionMathworldPlanetmath on P as follows.

  • 𝖼𝗈𝖽𝖾(ib,ib) is a set-quotient (see \autorefsec:set-quotients) of the type of sequencesPlanetmathPlanetmath



    • n:

    • xk:A and yk:A for 0<kn

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

    • pk:Π1B(fyk,fxk+1) for 1k<n

    • qk:Π1C(gxk,gyk) for 1kn

    The quotientPlanetmathPlanetmath is generated by the following equalities:

    (,qk,yk,𝗋𝖾𝖿𝗅fyk,yk,qk+1,) =(,qk\centerdotqk+1,)
    (,pk,xk,𝗋𝖾𝖿𝗅gxk,xk,pk+1,) =(,pk\centerdotpk+1,)

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

  • 𝖼𝗈𝖽𝖾(jc,jc) 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.

  • 𝖼𝗈𝖽𝖾(ib,jc) and 𝖼𝗈𝖽𝖾(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

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

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

    (,yn,pn,fa) (,yn,pn,a,𝗋𝖾𝖿𝗅ga,ga),
    (,xn,pn,a,𝗋𝖾𝖿𝗅fa,fa) \mapsfrom(,xn,pn,ga).

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


    which is equal to the identityPlanetmathPlanetmathPlanetmathPlanetmath 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

    𝖼𝗈𝖽𝖾(jc,ifa) 𝖼𝗈𝖽𝖾(jc,jga)
    𝖼𝗈𝖽𝖾(ifa,ib) (jga,ib)
    𝖼𝗈𝖽𝖾(ifa,jc) (jga,jc)

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

  • Finally, we need to know that for a,a:A, the following diagram commutes:

    \xymatrix 𝖼𝗈𝖽𝖾 (ifa,ifa’) \ar[r]\ar[d] & 𝖼𝗈𝖽𝖾 (ifa,jga’)\ar[d]
    𝖼𝗈𝖽𝖾 (jga,ifa’)\ar[r] & 𝖼𝗈𝖽𝖾 (jga,jga’)

    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 code some additional generating equations for the set-quotient, such as

(,pk-1\centerdotfw,xk,qk,) =(,pk-1,xk,gw\centerdotqk,) (for $w:\Pi_{1}A(x_{k},x_{k}^{\prime})$)
(,qk\centerdotgw,yk,pk,) =(,qk,yk,fw\centerdotpk,). (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 differencePlanetmathPlanetmath 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 fibrationMathworldPlanetmath 𝖼𝗈𝖽𝖾:

  • For p:b=Bb and u:P, we have

  • For q:c=Cc and u:P, we have


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


This follows essentially from the definition of 𝖼𝗈𝖽𝖾.

We also construct a function


by induction on u as follows:

rib :(b,𝗋𝖾𝖿𝗅b,b)
rjc :(c,𝗋𝖾𝖿𝗅c,c)

and for rka we take the composite equality

(ka,ka)*(fa,𝗋𝖾𝖿𝗅fa,fa) =(ga,𝗋𝖾𝖿𝗅ga,a,𝗋𝖾𝖿𝗅fa,a,𝗋𝖾𝖿𝗅ga,ga)

where the first equality is by the observation above about transporting in 𝖼𝗈𝖽𝖾, and the second is an instance of the set quotient relationMathworldPlanetmathPlanetmathPlanetmath used to define 𝖼𝗈𝖽𝖾.

We will now prove:

Theorem 8.7.4 (Naive van Kampen theorem).

For all u,v:P there is an equivalence


To define a function


it suffices to define a function (u=Pv)𝖼𝗈𝖽𝖾(u,v), since 𝖼𝗈𝖽𝖾(u,v) is a set. We do this by transport:


Now to define


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 pk and qk as appropriate and concatenate the results in P, using h to identify the endpoints. For instance, when uib and vib, we define

𝖽𝖾𝖼𝗈𝖽𝖾(b,p0,x1,q1,y1,p1,,yn,pn,b):(p0)\centerdoth(x1)\centerdotj(q1)\centerdoth(y1)-1\centerdoti(p1)\centerdot\centerdoth(yn)-1\centerdoti(pn). (8.7.5)

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

As usual, to show that the composite


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

Finally, consider the composite


We proceed by induction on u,v:P. When uib and vib, this composite is


i.e., the identity function. (To be precise, there is an implicit inductive argumentPlanetmathPlanetmath 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 groupsMathworldPlanetmathPlanetmath of many types, provided A is a set, for in that case, each 𝖼𝗈𝖽𝖾(u,v) is, by definition, a set-quotient of a set by a relation.

Example 8.7.5.

Let A:2, B:1, and C:1. Then PS1. Inspecting the definition of, say, code(i(),i()), we see that the paths all may as well be trivial, so the only information is in the sequence of elements x1,y1,,xn,yn:2. Moreover, if we have xk=yk or yk=xk+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 numberMathworldPlanetmath n) together with, if n>1, the information of whether x1 is 02 or 12, 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 x1 encodes the sign. Thus we recover π1(S1)Z.

Since \autorefthm:naive-van-kampen asserts only a bijection of families of sets, this isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath π1(S1) is likewise only a bijection of sets. We could, however, define a concatenation operationMathworldPlanetmath on 𝖼𝗈𝖽𝖾 (by concatenating sequences) and show that 𝖾𝗇𝖼𝗈𝖽𝖾 and 𝖽𝖾𝖼𝗈𝖽𝖾 form an isomorphism respecting this structureMathworldPlanetmath. (In the languagePlanetmathPlanetmath of \autorefcha:category-theory, these would be “pregroupoids”.) We leave the details to the reader.

Example 8.7.6.

More generally, let B:1 and C:1 but A be arbitrary, so that P is the suspension of A. Then once again the paths pk and qk are trivial, so that the only information in a path code is a sequence of elements x1,y1,,xn,yn: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


in a group. Indeed, it looks similar to the free groupMathworldPlanetmath on A (or equivalently on A0; 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 π1(ΣA) with the group presented by A0 as generatorsPlanetmathPlanetmath with the relation |a|0=e; see \autorefex:vksusppt,\autorefex:vksuspnopt for details.

Example 8.7.7.

Let A: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 BC of B and C (the coproductMathworldPlanetmath in the category of based spaces). In this case, it is the elements xk and yk which are trivial, so that the only information is a sequence of loops (p0,q1,p1,,pn) with pk:π1(B,b) and qk:π1(C,c). Such sequences, modulo the equivalence relation we have imposed, are easily identified with the explicit description of the free productMathworldPlanetmath of the groups π1(B,b) and π1(C,c), as constructed in \autorefsec:free-algebras. Thus, we have π1(BC)π1(B)*π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 π1(BAC)π1(B)*π1(A)π1(C) (with base point coming from A). Indeed, the conclusionMathworldPlanetmath of \autorefthm:naive-van-kampen says nothing at all about π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 𝖼𝗈𝖽𝖾(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