2.1 Types are higher groupoids

We now derive from the inductionMathworldPlanetmath principle the beginnings of the structureMathworldPlanetmath of a higher groupoidPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. We begin with symmetryPlanetmathPlanetmath of equality, which, in topological languagePlanetmathPlanetmath, means that “paths can be reversed”.

Lemma 2.1.1.

For every type A and every x,y:A there is a function


denoted pp-1, such that reflx-1reflx for each x:A. We call p-1 the inverseMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath of p.

Since this is our first time stating something as a “Lemma” or “Theorem”, let us pause to consider what that means. Recall that propositionsPlanetmathPlanetmath (statements susceptible to proof) are identified with types, whereas lemmas and theorems (statements that have been proven) are identified with inhabited types. Thus, the statement of a lemma or theorem should be translated into a type, as in §1.11 (http://planetmath.org/111propositionsastypes), and its proof translated into an inhabitant of that type. According to the interpretationMathworldPlanetmath of the universal quantifierMathworldPlanetmath “for every”, the type corresponding to Lemma 2.1.1 (http://planetmath.org/21typesarehighergroupoids#Thmprelem1) is


The proof of Lemma 2.1.1 (http://planetmath.org/21typesarehighergroupoids#Thmprelem1) will consist of constructing an element of this type, i.e. deriving the judgment f:(A:𝒰)(x,y:A)(x=y)(y=x) for some f. We then introduce the notation ()-1 for this element f, in which the arguments A, x, and y are omitted and inferred from context. (As remarked in §1.1 (http://planetmath.org/11typetheoryversussettheory), the secondary statement “𝗋𝖾𝖿𝗅x-1𝗋𝖾𝖿𝗅x for each x:A” should be regarded as a separate judgment.)

First proof.

Assume given A:𝒰, and let D:(x,y:A)(p:x=y)𝒰 be the type family defined by D(x,y,p):(y=x). In other words, D is a function assigning to any x,y:A and p:x=y a type, namely the type y=x. Then we have an element


Thus, the induction principle for identity types gives us an element 𝗂𝗇𝖽=A(D,d,x,y,p):(y=x) for each p:(x=y). We can now define the desired function ()-1 to be λp.𝗂𝗇𝖽=A(D,d,x,y,p), i.e. we set p-1:𝗂𝗇𝖽=A(D,d,x,y,p). The conversion rule (2.0.1) (http://planetmath.org/2homotopytypetheory#S0.E1) gives 𝗋𝖾𝖿𝗅x-1𝗋𝖾𝖿𝗅x, as required. ∎

We have written out this proof in a very formal style, which may be helpful while the induction rule on identity types is unfamiliar. To be even more formal, we could say that Lemma 2.1.1 (http://planetmath.org/21typesarehighergroupoids#Thmprelem1) and its proof together consist of the judgment


(along with an additional equality judgment). However, eventually we prefer to use more natural language, such as in the following equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath proof.

Second proof.

We want to construct, for each x,y:A and p:x=y, an element p-1:y=x. By induction, it suffices to do this in the case when y is x and p is 𝗋𝖾𝖿𝗅x. But in this case, the type x=y of p and the type y=x in which we are trying to construct p-1 are both simply x=x. Thus, in the “reflexivityMathworldPlanetmath case”, we can define 𝗋𝖾𝖿𝗅x-1 to be simply 𝗋𝖾𝖿𝗅x. The general case then follows by the induction principle, and the conversion rule 𝗋𝖾𝖿𝗅x-1𝗋𝖾𝖿𝗅x is precisely the proof in the reflexivity case that we gave. ∎

We will write out the next few proofs in both styles, to help the reader become accustomed to the latter one. Next we prove the transitivity of equality, or equivalently we “concatenate paths”.

Lemma 2.1.2.

For every type A and every x,y,z:A there is a function


written pqp\centerdotq, such that reflx\centerdotreflxreflx for any x:A. We call p\centerdotq the concatenationMathworldPlanetmath or composite of p and q.

First proof.

Let D:(x,y:A)(p:x=y)𝒰 be the type family


Note that D(x,x,𝗋𝖾𝖿𝗅x)(z:A)(q:x=z)(x=z). Thus, in order to apply the induction principle for identity types to this D, we need a function of type

x:AD(x,x,𝗋𝖾𝖿𝗅x) (2.1.3)

which is to say, of type


Now let E:(x,z:A)(q:x=z)𝒰 be the type family E(x,z,q):(x=z). Note that E(x,x,𝗋𝖾𝖿𝗅x)(x=x). Thus, we have the function


By the induction principle for identity types applied to E, we obtain a function


But E(x,z,q)(x=z), so this is (2.1.3). Thus, we can use this function d and apply the induction principle for identity types to D, to obtain our desired function of type


The conversion rules for the two induction principles give us 𝗋𝖾𝖿𝗅x\centerdot𝗋𝖾𝖿𝗅x𝗋𝖾𝖿𝗅x for any x:A. ∎

Second proof.

We want to construct, for every x,y,z:A and every p:x=y and q:y=z, an element of x=z. By induction on p, it suffices to assume that y is x and p is 𝗋𝖾𝖿𝗅x. In this case, the type y=z of q is x=z. Now by induction on q, it suffices to assume also that z is x and q is 𝗋𝖾𝖿𝗅x. But in this case, x=z is x=x, and we have 𝗋𝖾𝖿𝗅x:(x=x). ∎

The reader may well feel that we have given an overly convoluted proof of this lemma. In fact, we could stop after the induction on p, since at that point what we want to produce is an equality x=z, and we already have such an equality, namely q. Why do we go on to do another induction on q?

The answer is that, as described in the introduction, we are doing proof-relevant mathematics. When we prove a lemma, we are defining an inhabitant of some type, and it can matter what specific element we defined in the course of the proof, not merely the type inhabited by that element (that is, the statement of the lemma). Lemma 2.1.2 (http://planetmath.org/21typesarehighergroupoids#Thmprelem2) has three obvious proofs: we could do induction over p, induction over q, or induction over both of them. If we proved it three different ways, we would have three different elements of the same type. It’s not hard to show that these three elements are equal (see http://planetmath.org/node/87632Exercise 2.1), but as they are not definitionally equal, there can still be reasons to prefer one over another.

In the case of Lemma 2.1.2 (http://planetmath.org/21typesarehighergroupoids#Thmprelem2), the differencePlanetmathPlanetmath hinges on the computation rule. If we proved the lemma using a single induction over p, then we would end up with a computation rule of the form 𝗋𝖾𝖿𝗅y\centerdotqq. If we proved it with a single induction over q, we would have instead p\centerdot𝗋𝖾𝖿𝗅xp, while proving it with a double induction (as we did) gives only 𝗋𝖾𝖿𝗅x\centerdot𝗋𝖾𝖿𝗅x𝗋𝖾𝖿𝗅x.

The asymmetrical computation rules can sometimes be convenient when doing formalized mathematics, as they allow the computer to simplify more things automatically. However, in informal mathematics, and arguably even in the formalized case, it can be confusing to have a concatenation operationMathworldPlanetmath which behaves asymmetrically and to have to remember which side is the “special” one. Treating both sides symmetrically makes for more robust proofs; this is why we have given the proof that we did. (However, this is admittedly a stylistic choice.)

The table below summarizes the “equality”, “homotopical”, and “higher-groupoid” points of view on what we have done so far.

Equality Homotopy -Groupoid
reflexivity constant path identity morphism
symmetry inversion of paths inverse morphism
transitivity concatenation of paths composition of morphismsMathworldPlanetmathPlanetmath

In practice, transitivity is often applied to prove an equality by a chain of intermediate steps. We will use the common notation for this such as a=b=c=d. If the intermediate expressions are long, or we want to specify the witness of each equality, we may write

a =b (by p)
=c (by q)
=d (by r).

In either case, the notation indicates construction of the element (p\centerdotq)\centerdotr:(a=d). (We choose left-associativity for concreteness, although in view of Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(4) below it makes litle difference.) If it should happen that b and c, say, are judgmentally equal, then we may write

a =b (by p)
=d (by r)

to indicate construction of p\centerdotr:(a=d).

Now, because of proof-relevance, we can’t stop after proving “symmetry” and “transitivity” of equality: we need to know that these operations on equalities are well-behaved. (This issue is invisible in set theoryMathworldPlanetmath, where symmetry and transitivity are mere properties of equality, rather than structure on paths.) From the homotopy-theoretic point of view, concatenation and inversion are just the “first level” of higher groupoid structure — we also need coherence laws on these operations, and analogous operations at higher dimensionsMathworldPlanetmath. For instance, we need to know that concatenation is associative, and that inversion provides inverses with respect to concatenation.

Lemma 2.1.4.

Suppose A:U, that x,y,z,w:A and that p:x=y and q:y=z and r:z=w. We have the following:

  1. 1.

    p=p\centerdot𝗋𝖾𝖿𝗅y and p=𝗋𝖾𝖿𝗅x\centerdotp.

  2. 2.

    p-1\centerdotp=𝗋𝖾𝖿𝗅y and p\centerdotp-1=𝗋𝖾𝖿𝗅x.

  3. 3.


  4. 4.


Note, in particular, that 14 are themselves propositional equalities, living in the identity types of identity types, such as p=x=yq for p,q:x=y. Topologically, they are paths of paths, i.e. homotopies. It is a familiar fact in topologyMathworldPlanetmath that when we concatenate a path p with the reversed path p-1, we don’t literally obtain a constant path (which corresponds to the equality 𝗋𝖾𝖿𝗅 in type theoryPlanetmathPlanetmath) — instead we have a homotopy, or higher path, from p\centerdotp-1 to the constant path.

Proof of Lemma 3 (http://planetmath.org/21typesarehighergroupoids#Thmlem3).

All the proofs use the induction principle for equalities.

  1. 1.

    First proof: let D:(x,y:A)(p:x=y)𝒰 be the type family given by


    Then D(x,x,𝗋𝖾𝖿𝗅x) is 𝗋𝖾𝖿𝗅x=𝗋𝖾𝖿𝗅x\centerdot𝗋𝖾𝖿𝗅x. Since 𝗋𝖾𝖿𝗅x\centerdot𝗋𝖾𝖿𝗅x𝗋𝖾𝖿𝗅x, it follows that D(x,x,𝗋𝖾𝖿𝗅x)(𝗋𝖾𝖿𝗅x=𝗋𝖾𝖿𝗅x). Thus, there is a function


    Now the induction principle for identity types gives an element 𝗂𝗇𝖽=A(D,d,p):(p=p\centerdot𝗋𝖾𝖿𝗅y) for each p:x=y. The other equality is proven similarly.

    Second proof: by induction on p, it suffices to assume that y is x and that p is 𝗋𝖾𝖿𝗅x. But in this case, we have 𝗋𝖾𝖿𝗅x\centerdot𝗋𝖾𝖿𝗅x𝗋𝖾𝖿𝗅x.

  2. 2.

    First proof: let D:(x,y:A)(p:x=y)𝒰 be the type family given by


    Then D(x,x,𝗋𝖾𝖿𝗅x) is 𝗋𝖾𝖿𝗅x-1\centerdot𝗋𝖾𝖿𝗅x=𝗋𝖾𝖿𝗅x. Since 𝗋𝖾𝖿𝗅x-1𝗋𝖾𝖿𝗅x and 𝗋𝖾𝖿𝗅x\centerdot𝗋𝖾𝖿𝗅x𝗋𝖾𝖿𝗅x, we get that D(x,x,𝗋𝖾𝖿𝗅x)(𝗋𝖾𝖿𝗅x=𝗋𝖾𝖿𝗅x). Hence we find the function


    Now path induction gives an element 𝗂𝗇𝖽=A(D,d,p):p-1\centerdotp=𝗋𝖾𝖿𝗅y for each p:x=y in A. The other equality is similar.

    Second proof By induction, it suffices to assume p is 𝗋𝖾𝖿𝗅x. But in this case, we have p-1\centerdotp𝗋𝖾𝖿𝗅x-1\centerdot𝗋𝖾𝖿𝗅x𝗋𝖾𝖿𝗅x.

  3. 3.

    First proof: let D:(x,y:A)(p:x=y)𝒰 be the type family given by


    Then D(x,x,𝗋𝖾𝖿𝗅x) is the type (𝗋𝖾𝖿𝗅x-1-1=𝗋𝖾𝖿𝗅x). But since 𝗋𝖾𝖿𝗅x-1𝗋𝖾𝖿𝗅x for each x:A, we have 𝗋𝖾𝖿𝗅x-1-1𝗋𝖾𝖿𝗅x-1𝗋𝖾𝖿𝗅x, and thus D(x,x,𝗋𝖾𝖿𝗅x)(𝗋𝖾𝖿𝗅x=𝗋𝖾𝖿𝗅x). Hence we find the function


    Now path induction gives an element 𝗂𝗇𝖽=A(D,d,p):p-1-1=p for each p:x=y.

    Second proof: by induction, it suffices to assume p is 𝗋𝖾𝖿𝗅x. But in this case, we have p-1-1𝗋𝖾𝖿𝗅x-1-1𝗋𝖾𝖿𝗅x.

  4. 4.

    First proof: let D1:(x,y:A)(p:x=y)𝒰 be the type family given by


    Then D1(x,x,𝗋𝖾𝖿𝗅x) is


    To construct an element of this type, let D2:(x,z:A)(q:x=z)𝒰 be the type family


    Then D2(x,x,𝗋𝖾𝖿𝗅x) is


    To construct an element of this type, let D3:(x,w:A)(r:x=w)𝒰 be the type family


    Then D3(x,x,𝗋𝖾𝖿𝗅x) is


    which is definitionally equal to the type (𝗋𝖾𝖿𝗅x=𝗋𝖾𝖿𝗅x), and is therefore inhabited by 𝗋𝖾𝖿𝗅𝗋𝖾𝖿𝗅x. Applying the path induction rule three times, therefore, we obtain an element of the overall desired type.

    Second proof: by induction, it suffices to assume p, q, and r are all 𝗋𝖾𝖿𝗅x. But in this case, we have

    p\centerdot(q\centerdotr) 𝗋𝖾𝖿𝗅x\centerdot(𝗋𝖾𝖿𝗅x\centerdot𝗋𝖾𝖿𝗅x)

    Thus, we have 𝗋𝖾𝖿𝗅𝗋𝖾𝖿𝗅x inhabiting this type. ∎

Remark 2.1.5.

There are other ways to define these higher paths. For instance, in Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(4) we might do induction only over one or two paths rather than all three. Each possibility will produce a definitionally different proof, but they will all be equal to each other. Such an equality between any two particular proofs can, again, be proven by induction, reducing all the paths in question to reflexivities and then observing that both proofs reduce themselves to reflexivities.

In view of Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(4), we will often write p\centerdotq\centerdotr for (p\centerdotq)\centerdotr, and similarly p\centerdotq\centerdotr\centerdots for ((p\centerdotq)\centerdotr)\centerdots and so on. We choose left-associativity for definiteness, but it makes no real difference. We generally trust the reader to insert instances of Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(4) to reassociate such expressions as necessary.

We are still not really done with the higher groupoid structure: the paths 14 must also satisfy their own higher coherence laws, which are themselves higher paths, and so on “all the way up to infinityMathworldPlanetmath” (this can be made precise using e.g. the notion of a globular operad). However, for most purposes it is unnecessary to make the whole infinite-dimensional structure explicit. One of the nice things about homotopy type theory is that all of this structure can be proven starting from only the inductive property of identity types, so we can make explicit as much or as little of it as we need.

In particular, in this book we will not need any of the complicated combinatorics involved in making precise notions such as “coherent structure at all higher levels”. In addition to ordinary paths, we will use paths of paths (i.e. elements of a type p=x=Ayq), which as remarked previously we call 2-paths or 2-dimensional paths, and perhaps occasionally paths of paths of paths (i.e. elements of a type r=p=x=Ayqs), which we call 3-paths or 3-dimensional paths. It is possible to define a general notion of n-dimensional path (see http://planetmath.org/node/87635Exercise 2.4), but we will not need it.

We will, however, use one particularly important and simple case of higher paths, which is when the start and end points are the same. In set theory, the proposition a=a is entirely uninteresting, but in homotopy theory, paths from a point to itself are called loops and carry lots of interesting higher structure. Thus, given a type A with a point a:A, we define its loop spaceMathworldPlanetmath Ω(A,a) to be the type a=Aa. We may sometimes write simply ΩA if the point a is understood from context.

Since any two elements of ΩA are paths with the same start and end points, they can be concatenated; thus we have an operation ΩA×ΩAΩA. More generally, the higher groupoid structure of A gives ΩA the analogous structure of a “higher group”.

It can also be useful to consider the loop space of the loop space of A, which is the space of 2-dimensional loops on the identity loop at a. This is written Ω2(A,a) and represented in type theory by the type 𝗋𝖾𝖿𝗅a=(a=Aa)𝗋𝖾𝖿𝗅a. While Ω2(A,a), as a loop space, is again a “higher group”, it now also has some additional structure resulting from the fact that its elements are 2-dimensional loops between 1-dimensional loops.

Theorem 2.1.6 (Eckmann–Hilton).

The composition operation on the second loop space


is commutativePlanetmathPlanetmathPlanetmathPlanetmath: α\centerdotβ=β\centerdotα, for any α,β:Ω2(A).


First, observe that the composition of 1-loops ΩA×ΩAΩA induces an operation


as follows: consider elements a,b,c:A and 1- and 2-paths,

p :a=b, r :b=c
q :a=b, s :b=c
α :p=q, β :r=s

as depicted in the following diagram (with paths drawn as arrows).



Composing the upper and lower 1-paths, respectively, we get two paths p\centerdotr,q\centerdots:a=c, and there is then a “horizontal compositionPlanetmathPlanetmath


between them, defined as follows. First, we define \centerdotrαr:p\centerdotr=q\centerdotr by path induction on r, so that


where 𝗋𝗎p:p=p\centerdot𝗋𝖾𝖿𝗅b is the right unit law from Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(1). We could similarly define \centerdotr by induction on α, or on all paths in sight, resulting in different judgmental equalities, but for present purposes the definition by induction on r will make things simpler. Similarly, we define \centerdotqβ:q\centerdotr=q\centerdots by induction on q, so that


where 𝗅𝗎r denotes the left unit law. The operations \centerdot and \centerdotr are called whiskering. Next, since \centerdotrαr and \centerdotqβ are composable 2-paths, we can define the horizontal composition by:


Now suppose that abc, so that all the 1-paths p, q, r, and s are elements of Ω(A,a), and assume moreover that pqrs𝗋𝖾𝖿𝗅a, so that α:𝗋𝖾𝖿𝗅a=𝗋𝖾𝖿𝗅a and β:𝗋𝖾𝖿𝗅a=𝗋𝖾𝖿𝗅a are composable in both orders. In that case, we have

αβ (\centerdotrα𝗋𝖾𝖿𝗅a)\centerdot(\centerdot𝗋𝖾𝖿𝗅aβ)

(Recall that 𝗋𝗎𝗋𝖾𝖿𝗅a𝗅𝗎𝗋𝖾𝖿𝗅a𝗋𝖾𝖿𝗅𝗋𝖾𝖿𝗅a, by the computation rule for path induction.) On the other hand, we can define another horizontal composition analogously by


and we similarly learn that


But, in general, the two ways of defining horizontal composition agree, αβ=αβ, as we can see by induction on α and β and then on the two remaining 1-paths, to reduce everything to reflexivity. Thus we have


The foregoing fact, which is known as the Eckmann–Hilton argument, comes from classical homotopy theory, and indeed it is used in http://planetmath.org/node/87582Chapter 8 below to show that the higher homotopy groups of a type are always abelian groups. The whiskering and horizontal composition operations defined in the proof are also a general part of the -groupoid structure of types. They satisfy their own laws (up to higher homotopy), such as


and so on. From now on, we trust the reader to apply path induction whenever needed to define further operations of this sort and verify their properties.

As this example suggests, the algebraPlanetmathPlanetmath of higher path types is much more intricate than just the groupoid-like structure at each level; the levels interact to give many further operations and laws, as in the study of iterated loop spaces in homotopy theory. Indeed, as in classical homotopy theory, we can make the following general definitions:

Definition 2.1.7.

A pointed type (A,a) is a type A:U together with a point a:A, called its basepoint. We write U:(A:U)A for the type of pointed types in the universePlanetmathPlanetmath U.

Definition 2.1.8.

Given a pointed type (A,a), we define the loop space of (A,a) to be the following pointed type:


An element of it will be called a loop at a. For n:N, the n-fold iterated loop space Ωn(A,a) of a pointed type (A,a) is defined recursively by:

Ω0(A,a) :(A,a)
Ωn+1(A,a) :Ωn(Ω(A,a)).

An element of it will be called an n-loop or an n-dimensional loop at a.

We will return to iterated loop spaces in http://planetmath.org/node/87580Chapter 7,http://planetmath.org/node/87579Chapter 6,http://planetmath.org/node/87582Chapter 8.

Title 2.1 Types are higher groupoids