6.11 Algebra

In addition 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 colimit of any diagram of sets, which is not possible in the base type theory of http://planetmath.org/node/87533Chapter 1. Higher inductive types are also very useful when we study sets with algebraic structure.

As a running example in this section, 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\times G\to G$ , written infix as $(x,y)\mapsto x\cdot y$ ; and
•

a unit element $e : G$ ; such that
•

for any $x : G$ , we have $x\cdot e=x$ and $e\cdot x=x$ ; and
•

for any $x, y, z : G$ , we have $x\cdot(y\cdot z)=(x\cdot y)\cdot z$ .

A group is a monoid $G$ together with

•

an inversion function $i:G\to G$ , written $x\mapsto\mathord{{x}^{-1}}$ ; such that
•

for any $x : G$ we have $x\cdot\mathord{{x}^{-1}}=e$ and $\mathord{{x}^{-1}}\cdot x=e$ .

Remark 6.11.2.

Note that we require a group to be a set. We could consider a more general notion of “ $\infty$ -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 $\mathsf{LEM}$ , it will be “constructive” group theory).

Example 6.11.3.

The natural numbers $\mathbb{N}$ are a monoid under addition, with unit $0$ , and also under multiplication, with unit $1$ . If we define the arithmetical operations on the integers $\mathbb{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,v\in\mathbb{Z}$ 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 $u v$ 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 $\Omega(A,a):\!\!\equiv(a=_{A}a)$ has all the structure of a group, except that it is not in general a set. It should be an “ $\infty$ -group” in the sense mentioned in Remark 6.11.2 (http://planetmath.org/611algebra#Thmprermk1), but we can also make it a group by truncation. Specifically, we define the fundamental group of $A$ based at $a : A$ to be

\pi_{1}(A,a):\!\!\equiv\mathopen{}\left\|\Omega(A,a)\right\|_{0}\mathclose{}.

This inherits a group structure; for instance, the multiplication $\pi_{1}(A,a)\times\pi_{1}(A,a)\to\pi_{1}(A,a)$ is defined by double induction on truncation from the concatenation of paths.

More generally, the $n^{\mathrm{th}}$ homotopy group of $(A,a)$ is $\pi_{n}(A,a):\!\!\equiv\mathopen{}\left\|\Omega^{n}(A,a)\right\|_{0}\mathclose{}$ . Then $\pi_{n}(A,a)=\pi_{1}(\Omega^{n-1}(A,a))$ for $n\geq 1$ , so it is also a group. (When $n=0$ , we have $\pi_{0}(A)\equiv\mathopen{}\left\|A\right\|_{0}\mathclose{}$ , which is not a group.) Moreover, the Eckmann–Hilton argument (Remark 1 (http://planetmath.org/21typesarehighergroupoids#Thmrmk1)) implies that if $n\geq 2$ , then $\pi_{n}(A,a)$ is an abelian group, i.e. we have $x\cdot y=y\cdot x$ 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 group 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 $\mathsf{List}(A)$ of finite lists of elements of $A$ , which is inductively generated by

•

a constructor $\mathsf{nil}:\mathsf{List}(A)$ , and
•

for each $\ell:\mathsf{List}(A)$ and $a : A$ , an element $\mathsf{cons}(a,\ell):\mathsf{List}(A)$ .

We have an obvious inclusion $\eta:A\to\mathsf{List}(A)$ defined by $a\mapsto\mathsf{cons}(a,\mathsf{nil})$ . The monoid operation on $\mathsf{List}(A)$ is concatenation, defined recursively by

	$\displaystyle\mathsf{nil}\cdot\ell$	$\displaystyle:\!\!\equiv\ell$
	$\displaystyle\mathsf{cons}(a,\ell_{1})\cdot\ell_{2}$	$\displaystyle:\!\!\equiv\mathsf{cons}(a,\ell_{1}\cdot\ell_{2}).$

It is straightforward to prove, using the induction principle for $\mathsf{List}(A)$ , that $\mathsf{List}(A)$ is a set and that concatenation of lists is associative and has $\mathsf{nil}$ as a unit. Thus, $\mathsf{List}(A)$ is a monoid.

Lemma 6.11.5.

For any set $A$ , the type $\mathsf{List}(A)$ is the free monoid on $A$ . In other words, for any monoid $G$ , composition with $\eta$ is an equivalence

\hom_{\mathrm{Monoid}}(\mathsf{List}(A),G)\simeq(A\to G),

where $\hom_{\mathrm{Monoid}}(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt})$ denotes the set of monoid homomorphisms (functions which preserve the multiplication and unit).

Proof.

Given $f:A\to G$ , we define $\bar{f}:\mathsf{List}(A)\to G$ by recursion:

	$\displaystyle\bar{f}(\mathsf{nil})$	$\displaystyle:\!\!\equiv e$
	$\displaystyle\bar{f}(\mathsf{cons}(a,\ell))$	$\displaystyle:\!\!\equiv f(a)\cdot\bar{f}(\ell).$

It is straightforward to prove by induction that $\bar{f}$ is a monoid homomorphism, and that $f\mapsto\bar{f}$ is a quasi-inverse of $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ\eta)$ ; 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 generators.

•

A function $\eta:A\to F(A)$ .
•

A function $m:F(A)\times F(A)\to F(A)$ .
•

An element $e:F(A)$ .
•

A function $i:F(A)\to 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 element, and inversion. The three constructors after that assert the axioms of a group: associativity, unitality, and inverses. 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 $\eta:A\to F(A)$ determines an equivalence

\hom_{\mathrm{Group}}(F(A),G)\simeq(A\to G)

where $\hom_{\mathrm{Group}}(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt})$ denotes the set of group homomorphisms between two groups.

Proof.

The recursion principle of the higher inductive type $F(A)$ says precisely that if $G$ is a group and we have $f:A\to G$ , then we have $\bar{f}:F(A)\to G$ . Its computation rules say that $\bar{f}\circ\eta\equiv f$ , and that $\bar{f}$ is a group homomorphism. Thus, $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ\eta):\hom_{\mathrm{Group}}(F% (A),G)\to(A\to G)$ 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 property that it should satisfy. In set theory, we could achieve a similar 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 quotients. Consider $\mathsf{List}(A+A)$ , where in $A+A$ we write ${\mathsf{inl}}(a)$ as $a$ , and ${\mathsf{inr}}(a)$ as $\hat{a}$ (intended to stand for the formal inverse of $a$ ). The elements of $\mathsf{List}(A+A)$ are words for the free group on $A$ .

Theorem 6.11.7.

Let $A$ be a set, and let $F^{\prime}(A)$ be the set-quotient of $\mathsf{List}(A+A)$ by the following relations.

	$\displaystyle(\dots,a_{1},a_{2},\widehat{a_{2}},a_{3},\dots)$	$\displaystyle=(\dots,a_{1},a_{3},\dots)$
	$\displaystyle(\dots,a_{1},\widehat{a_{2}},a_{2},a_{3},\dots)$	$\displaystyle=(\dots,a_{1},a_{3},\dots).$

Then $F^{\prime}(A)$ is also the free group on the set $A$ .

Proof.

First we show that $F^{\prime}(A)$ is a group. We have seen that $\mathsf{List}(A+A)$ is a monoid; we claim that the monoid structure descends to the quotient. We define $F^{\prime}(A)\times F^{\prime}(A)\to F^{\prime}(A)$ by double quotient recursion; it suffices to check that the equivalence relation 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^{\prime}(A)$ , we first define $\mathsf{reverse}:\mathsf{List}(B)\to\mathsf{List}(B)$ by recursion on lists:

	$\displaystyle\mathsf{reverse}(\mathsf{nil})$	$\displaystyle:\!\!\equiv\mathsf{nil},$
	$\displaystyle\mathsf{reverse}(\mathsf{cons}(b,\ell))$	$\displaystyle:\!\!\equiv\mathsf{reverse}(\ell)\cdot\mathsf{cons}(b,\mathsf{nil% }).$

Now we define $i:F^{\prime}(A)\to F^{\prime}(A)$ by quotient recursion, acting on a list $\ell:\mathsf{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)\cdot x=e$ for $x:F^{\prime}(A)$ by induction. First, quotient induction allows us to assume $x$ comes from $\ell:\mathsf{List}(A+A)$ , and then we can do list induction:

$\displaystyle i(\mathsf{nil})\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{nil}$	$\displaystyle=\mathsf{nil}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{nil}$
	$\displaystyle=\mathsf{nil}$
$\displaystyle i(\mathsf{cons}(a,\ell))\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{cons}(a,\ell)$	$\displaystyle=i(\ell)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{cons}(\hat{a},\mathsf{nil})% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\mathsf{cons}(a,\ell)$
	$\displaystyle=i(\ell)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{cons}(\hat{a},\mathsf{cons}(a,\ell))$
	$\displaystyle=i(\ell)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\ell$
	$\displaystyle=\mathsf{nil}.{}$	(by the inductive hypothesis)

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

This completes the proof that $F^{\prime}(A)$ is a group. Now if $G$ is any group with a function $f:A\to G$ , we can define $A+A\to G$ 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 $\mathsf{List}(A+A)\to G$ . And since $G$ is a group, this map respects the relations, hence descends to a map $F^{\prime}(A)\to 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^{\prime}(A)$ can be obtained from an idempotent as in Lemma 6.10.8 (http://planetmath.org/610quotients#Thmprelem3). We define a word, which we recall is just an element of $\mathsf{List}(A+A)$ , to be reduced if it contains no adjacent pairs of the form $(a,\hat{a})$ or $(\hat{a},a)$ . When $A$ has decidable equality, it is straightforward to define the reduction of a word, which is an idempotent generating the appropriate quotient; we leave the details to the reader.

If $A:\!\!\equiv\mathbf{1}$ , which has decidable equality, a reduced word must consist either entirely of $\star$ ’s or entirely of $\hat{\star}$ ’s. Thus, the free group on $\mathbf{1}$ is equivalent to the integers $\mathbb{Z}$ , with $0$ corresponding to $\mathsf{nil}$ , the positive integer $n$ corresponding to a reduced word of $n$ $\star$ ’s, and the negative integer $(-n)$ corresponding to a reduced word of $n$ $\hat{\star}$ ’s. One could also, of course, show directly that $\mathbb{Z}$ has the universal property of $F(\mathbf{1})$ .

Remark 6.11.8.

Nowhere in the construction of $F(A)$ and $F^{\prime}(A)$ , and the proof of their universal properties, did we use the assumption 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)\simeq F(\mathopen{}\left\|A\right\|_{0}\mathclose{})$ .

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

•

Functions $h:H\to H*_{G}K$ and $k:K\to H*_{G}K$ .
•

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 $\mathsf{List}(H+K)$ by the following relations:

$\displaystyle(\dots,x_{1},x_{2},\dots)$	$\displaystyle=(\dots,x_{1}\cdot x_{2},\dots)$	for $x_{1},x_{2}:H$
$\displaystyle(\dots,y_{1},y_{2},\dots)$	$\displaystyle=(\dots,y_{1}\cdot y_{2},\dots)$	for $y_{1},y_{2}:K$
$\displaystyle(\dots,1_{G},\dots)$	$\displaystyle=(\dots,\dots)$
$\displaystyle(\dots,1_{H},\dots)$	$\displaystyle=(\dots,\dots)$
$\displaystyle(\dots,f(x),\dots)$	$\displaystyle=(\dots,g(x),\dots)$	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 product $H*K$ , the coproduct 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 presentations 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\rightrightarrows F(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 $\langle a\mid a^{2}=e\rangle$ we would have $A:\!\!\equiv\mathbf{1}$ and $R:\!\!\equiv\mathbf{1}$ , with the two morphisms $R\rightrightarrows F(A)$ picking out the list $(a,a)$ and the empty list $\mathsf{nil}$ , respectively. Then by the universal property of free groups, we obtain a pair of group homomorphisms $F(R)\rightrightarrows F(A)$ . Their coequalizer 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 variables, 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\mathrel{\#}0\}$ specified by an apartness $\#$ between previous operations, see Theorem 11.2.4 (http://planetmath.org/1122dedekindrealsarecauchycomplete#Thmprethm1). And indeed, it is well-known that the category of fields has no initial object.

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 algebras as a simple quotient, unless we assume the axiom of choice. 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
\metatable