6.11 Algebra

In additionPlanetmathPlanetmath to constructing higher-dimensional objects such as spheres and cell complexes, higher inductive types are also very useful even when working only with sets. We have seen one example already in Lemma 6.9.3 (http://planetmath.org/69truncations#Thmprelem3): they allow us to construct the colimitMathworldPlanetmath of any diagram of sets, which is not possible in the base type theoryPlanetmathPlanetmath of http://planetmath.org/node/87533Chapter 1. Higher inductive types are also very useful when we study sets with algebraic structurePlanetmathPlanetmath.

As a running example in this sectionMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we consider groups, which are familiar to most mathematicians and exhibit the essential phenomena (and will be needed in later chapters). However, most of what we say applies equally well to any sort of algebraic structure.

Definition 6.11.1.

A monoid is a set G together with

  • a multiplication function G×GG, written infix as (x,y)xy; and

  • a unit element e:G; such that

  • for any x:G, we have xe=x and ex=x; and

  • for any x,y,z:G, we have x(yz)=(xy)z.

A group is a monoid G together with

  • an inversionMathworldPlanetmathPlanetmath function i:GG, written xx-1; such that

  • for any x:G we have xx-1=e and x-1x=e.

Remark 6.11.2.

Note that we require a group to be a set. We could consider a more general notion of “-group” which is not a set, but this would take us further afield than is appropriate at the moment. With our current definition, we may expect the resulting “group theory” to behave similarly to the way it does in set-theoretic mathematics (with the caveat that, unless we assume LEM, it will be “constructive” group theory).

Example 6.11.3.

The natural numbersMathworldPlanetmath N are a monoid under addition, with unit 0, and also under multiplication, with unit 1. If we define the arithmetical operationsMathworldPlanetmath on the integers Z in the obvious way, then as usual they are a group under addition and a monoid under multiplication (and, of course, a ring). For instance, if u,vZ are represented by (a,b) and (c,d), respectively, then u+v is represented by (a+c,b+d), -u is represented by (b,a), and uv is represented by (ac+bd,ad+bc).

Example 6.11.4.

We essentially observed in §2.1 (http://planetmath.org/21typesarehighergroupoids) that if (A,a) is a pointed type, then its loop space Ω(A,a):(a=Aa) has all the structureMathworldPlanetmath of a group, except that it is not in general a set. It should be an “-group” in the sense mentioned in Remark 6.11.2 (http://planetmath.org/611algebra#Thmprermk1), but we can also make it a group by truncationMathworldPlanetmath. Specifically, we define the fundamental groupMathworldPlanetmathPlanetmath of A based at a:A to be


This inherits a group structure; for instance, the multiplication π1(A,a)×π1(A,a)π1(A,a) is defined by double inductionMathworldPlanetmath on truncation from the concatenation of paths.

More generally, the nth homotopy group of (A,a) is πn(A,a):Ωn(A,a)0. Then πn(A,a)=π1(Ωn-1(A,a)) for n1, so it is also a group. (When n=0, we have π0(A)A0, which is not a group.) Moreover, the Eckmann–Hilton argument (Remark 1 (http://planetmath.org/21typesarehighergroupoids#Thmrmk1)) implies that if n2, then πn(A,a) is an abelianMathworldPlanetmath group, i.e. we have xy=yx for all x,y. http://planetmath.org/node/87582Chapter 8 will be largely the study of these groups.

One important notion in group theory is that of the free groupMathworldPlanetmath generated by a set, or more generally of a group presented by generators and relations. It is well-known in type theory that some free algebraic objects can be defined using ordinary inductive types. For instance, the free monoid on a set A can be identified with the type 𝖫𝗂𝗌𝗍(A) of finite lists of elements of A, which is inductively generated by

  • a constructor 𝗇𝗂𝗅:𝖫𝗂𝗌𝗍(A), and

  • for each :𝖫𝗂𝗌𝗍(A) and a:A, an element 𝖼𝗈𝗇𝗌(a,):𝖫𝗂𝗌𝗍(A).

We have an obvious inclusion η:A𝖫𝗂𝗌𝗍(A) defined by a𝖼𝗈𝗇𝗌(a,𝗇𝗂𝗅). The monoid operation on 𝖫𝗂𝗌𝗍(A) is concatenation, defined recursively by

𝗇𝗂𝗅 :
𝖼𝗈𝗇𝗌(a,1)2 :𝖼𝗈𝗇𝗌(a,12).

It is straightforward to prove, using the induction principle for 𝖫𝗂𝗌𝗍(A), that 𝖫𝗂𝗌𝗍(A) is a set and that concatenation of lists is associative and has 𝗇𝗂𝗅 as a unit. Thus, 𝖫𝗂𝗌𝗍(A) is a monoid.

Lemma 6.11.5.

For any set A, the type List(A) is the free monoid on A. In other words, for any monoid G, composition with η is an equivalence


where homMonoid(,) denotes the set of monoid homomorphisms (functions which preserve the multiplication and unit).


Given f:AG, we define f¯:𝖫𝗂𝗌𝗍(A)G by recursion:

f¯(𝗇𝗂𝗅) :e
f¯(𝖼𝗈𝗇𝗌(a,)) :f(a)f¯().

It is straightforward to prove by induction that f¯ is a monoid homomorphism, and that ff¯ is a quasi-inverse of (η); see http://planetmath.org/node/87876Exercise 6.8. ∎

This construction of the free monoid is possible essentially because elements of the free monoid have computable canonical forms (namely, finite lists). However, elements of other free (and presented) algebraic structures — such as groups — do not in general have computable canonical forms. For instance, equality of words in group presentations is algorithmically undecidable. However, we can still describe free algebraic objects as higher inductive types, by simply asserting all the axiomatic equations as path constructors.

For example, let A be a set, and define a higher inductive type F(A) with the following generatorsPlanetmathPlanetmathPlanetmath.

  • A function η:AF(A).

  • A function m:F(A)×F(A)F(A).

  • An element e:F(A).

  • A function i:F(A)F(A).

  • For each x,y,z:F(A), an equality m(x,m(y,z))=m(m(x,y),z).

  • For each x:F(A), equalities m(x,e)=x and m(e,x)=x.

  • For each x:F(A), equalities m(x,i(x))=e and m(i(x),x)=e.

  • The 0-truncation constructor: for any x,y:F(A) and p,q:x=y, we have p=q.

The first constructor says that A maps to F(A). The next three give F(A) the operations of a group: multiplication, an identity elementMathworldPlanetmath, and inversion. The three constructors after that assert the axioms of a group: associativity, unitality, and inversesMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. Finally, the last constructor asserts that F(A) is a set.

Therefore, F(A) is a group. It is also straightforward to prove:

Theorem 6.11.6.

F(A) is the free group on A. In other words, for any (set) group G, composition with η:AF(A) determines an equivalence


where homGroup(,) denotes the set of group homomorphismsMathworldPlanetmath between two groups.


The recursion principle of the higher inductive type F(A) says precisely that if G is a group and we have f:AG, then we have f¯:F(A)G. Its computation rules say that f¯ηf, and that f¯ is a group homomorphism. Thus, (η):homGroup(F(A),G)(AG) has a right inverse. It is straightforward to use the induction principle of F(A) to show that this is also a left inverse. ∎

It is worth taking a step back to consider what we have just done. We have proven that the free group on any set exists without giving an explicit construction of it. Essentially all we had to do was write down the universal propertyMathworldPlanetmath that it should satisfy. In set theoryMathworldPlanetmath, we could achieve a similarMathworldPlanetmathPlanetmath result by appealing to black boxes such as the adjoint functor theorem; type theory builds such constructions into the foundations of mathematics.

Of course, it is sometimes also useful to have a concrete description of free algebraic structures. In the case of free groups, we can provide one, using quotientsPlanetmathPlanetmath. Consider 𝖫𝗂𝗌𝗍(A+A), where in A+A we write 𝗂𝗇𝗅(a) as a, and 𝗂𝗇𝗋(a) as a^ (intended to stand for the formal inverse of a). The elements of 𝖫𝗂𝗌𝗍(A+A) are words for the free group on A.

Theorem 6.11.7.

Let A be a set, and let F(A) be the set-quotient of List(A+A) by the following relationsMathworldPlanetmathPlanetmath.

(,a1,a2,a2^,a3,) =(,a1,a3,)
(,a1,a2^,a2,a3,) =(,a1,a3,).

Then F(A) is also the free group on the set A.


First we show that F(A) is a group. We have seen that 𝖫𝗂𝗌𝗍(A+A) is a monoid; we claim that the monoid structure descends to the quotient. We define F(A)×F(A)F(A) by double quotient recursion; it suffices to check that the equivalence relationMathworldPlanetmath generated by the given relations is preserved by concatenation of lists. Similarly, we prove the associativity and unit laws by quotient induction.

In order to define inverses in F(A), we first define 𝗋𝖾𝗏𝖾𝗋𝗌𝖾:𝖫𝗂𝗌𝗍(B)𝖫𝗂𝗌𝗍(B) by recursion on lists:

𝗋𝖾𝗏𝖾𝗋𝗌𝖾(𝗇𝗂𝗅) :𝗇𝗂𝗅,
𝗋𝖾𝗏𝖾𝗋𝗌𝖾(𝖼𝗈𝗇𝗌(b,)) :𝗋𝖾𝗏𝖾𝗋𝗌𝖾()𝖼𝗈𝗇𝗌(b,𝗇𝗂𝗅).

Now we define i:F(A)F(A) by quotient recursion, acting on a list :𝖫𝗂𝗌𝗍(A+A) by switching the two copies of A and reversing the list. This preserves the relations, hence descends to the quotient. And we can prove that i(x)x=e for x:F(A) by induction. First, quotient induction allows us to assume x comes from :𝖫𝗂𝗌𝗍(A+A), and then we can do list induction:

i(𝗇𝗂𝗅)\centerdot𝗇𝗂𝗅 =𝗇𝗂𝗅\centerdot𝗇𝗂𝗅
i(𝖼𝗈𝗇𝗌(a,))\centerdot𝖼𝗈𝗇𝗌(a,) =i()\centerdot𝖼𝗈𝗇𝗌(a^,𝗇𝗂𝗅)\centerdot𝖼𝗈𝗇𝗌(a,)
=𝗇𝗂𝗅. (by the inductive hypothesis)

(We have omitted a number of fairly evident lemmas about the behavior of concatenation of lists, etc.)

This completesPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath the proof that F(A) is a group. Now if G is any group with a function f:AG, we can define A+AG to be f on the first copy of A and f composed with the inversion map of G on the second copy. Now the fact that G is a monoid yields a monoid homomorphism 𝖫𝗂𝗌𝗍(A+A)G. And since G is a group, this map respects the relations, hence descends to a map F(A)G. It is straightforward to prove that this is a group homomorphism, and the unique one which restricts to f on A. ∎

If A has decidable equality (such as if we assume excluded middle), then the quotient defining F(A) can be obtained from an idempotentMathworldPlanetmathPlanetmath as in Lemma 6.10.8 (http://planetmath.org/610quotients#Thmprelem3). We define a word, which we recall is just an element of 𝖫𝗂𝗌𝗍(A+A), to be reduced if it contains no adjacentPlanetmathPlanetmath pairs of the form (a,a^) or (a^,a). When A has decidable equality, it is straightforward to define the reductionPlanetmathPlanetmath of a word, which is an idempotent generating the appropriate quotient; we leave the details to the reader.

If A:𝟏, which has decidable equality, a reduced word must consist either entirely of ’s or entirely of ^’s. Thus, the free group on 𝟏 is equivalentMathworldPlanetmathPlanetmath to the integers , with 0 corresponding to 𝗇𝗂𝗅, the positive integer n corresponding to a reduced word of n ’s, and the negative integer (-n) corresponding to a reduced word of n ^’s. One could also, of course, show directly that has the universal property of F(𝟏).

Remark 6.11.8.

Nowhere in the construction of F(A) and F(A), and the proof of their universal properties, did we use the assumptionPlanetmathPlanetmath that A is a set. Thus, we can actually construct the free group on an arbitrary type. Comparing universal properties, we conclude that F(A)F(A0).

We can also use higher inductive types to construct colimits of algebraic objects. For instance, suppose f:GH and g:GK are group homomorphisms. Their pushout in the category of groups, called the amalgamated free product H*GK, can be constructed as the higher inductive type generated by

  • Functions h:HH*GK and k:KH*GK.

  • The operations and axioms of a group, as in the definition of F(A).

  • Axioms asserting that h and k are group homomorphisms.

  • For x:G, we have h(f(x))=k(g(x)).

  • The 0-truncation constructor.

On the other hand, it can also be constructed explicitly, as the set-quotient of 𝖫𝗂𝗌𝗍(H+K) by the following relations:

(,x1,x2,) =(,x1x2,) for x1,x2:H
(,y1,y2,) =(,y1y2,) for y1,y2:K
(,1G,) =(,)
(,1H,) =(,)
(,f(x),) =(,g(x),) for x:G.

We leave the proofs to the reader. In the special case that G is the trivial group, the last relation is unnecessary, and we obtain the free productMathworldPlanetmath H*K, the coproductMathworldPlanetmath in the category of groups. (This notation unfortunately clashes with that for the join of types, as in §6.8 (http://planetmath.org/68pushouts), but context generally disambiguates.)

Note that groups defined by presentationsMathworldPlanetmathPlanetmath can be regarded as a special case of colimits. Suppose given a set (or more generally a type) A, and a pair of functions R\rightrightarrowsF(A). We regard R as the type of “relations”, with the two functions assigning to each relation the two words that it sets equal. For instance, in the presentation aa2=e we would have A:𝟏 and R:𝟏, with the two morphismsMathworldPlanetmathPlanetmath R\rightrightarrowsF(A) picking out the list (a,a) and the empty list 𝗇𝗂𝗅, respectively. Then by the universal property of free groups, we obtain a pair of group homomorphisms F(R)\rightrightarrowsF(A). Their coequalizerMathworldPlanetmath in the category of groups, which can be built just like the pushout, is the group presented by this presentation.

Note that all these sorts of construction only apply to algebraic theories, which are theories whose axioms are (universally quantified) equations referring to variablesMathworldPlanetmath, constants, and operations from a given signature. They can be modified to apply also to what are called essentially algebraic theories: those whose operations are partially defined on a domain specified by equalities between previous operations. They do not apply, for instance, to the theory of fields, in which the “inversion” operation is partially defined on a domain {x|x#0} specified by an apartness # between previous operations, see TheoremMathworldPlanetmath 11.2.4 (http://planetmath.org/1122dedekindrealsarecauchycomplete#Thmprethm1). And indeed, it is well-known that the category of fields has no initial objectMathworldPlanetmath.

On the other hand, these constructions do apply just as well to infinitary algebraic theories, whose “operations” can take infinitely many inputs. In such cases, there may not be any presentation of free algebras or colimits of algebrasMathworldPlanetmathPlanetmathPlanetmath as a simple quotient, unless we assume the axiom of choiceMathworldPlanetmath. This means that higher inductive types represent a significant strengthening of constructive type theory (not necessarily in terms of proof-theoretic strength, but in terms of practical power), and indeed are stronger in some ways than Zermelo–Fraenkel set theory (without choice).

Title 6.11 Algebra