François G. Dorais

Research in Logic and Foundations of Mathematics


HoTT Math 1: Elementary group theory

This is the first in a series of posts on doing mathematics in Homotopy Type Theory (HoTT). Various conventions and notations are explained in the preamble; there are no additional prerequisites for this post.


A group is a set equipped with a constant , a unary operation and a binary operation that satisfy the usual axioms. In HoTT the group axioms must be motivated, so the group comes with three more components:

The axioms are concrete objects in proof-relevant mathematics! The last two axioms are actually the conjunction of two axioms since conjunction in HoTT correspond to products. It’s conceptually convenient to package them together and use and for the two conjuncts obtained by applying the projections. In fact, it makes sense to pack all of these into one

(but, for the sake of clarity, it is best to refrain from using things like for ).

The axioms types above are parametrized by and the three components , , , so one can form the type of all groups:

This level of formalism is cumbersome and since it is perfectly clear what the type is from the narrative description, it is best to avoid it. The only difference from classical mathematics is that the axioms are given as concrete objects rather than abstract statements.

Familiar identities, for example the fact that is its own inverse, can be obtained by combining the group axioms. We have a path and another path . Concatenating these two paths yields the desired path

There are other ways to see this, for example, symmetric reasoning yields

In general, these two paths are need not be the same but since is a set, i.e., a 0-type, there is at most one path in and therefore the two paths above must be the same.

Let’s try something a tad more complicated — an old favorite — the uniqueness of identity elements. To say that is a left identity element means exhibiting an element of the type

so shows that is an identity element. Similarly, shows that is a right identity element. Classically, we know that if is a left identity and if is a right identity then we must have . In HoTT, this corresponds to exhibiting an element of type

To prove this, let’s fix . Given and we have paths

and therefore a path

The classical proof would end here but to get the desired element of , we need to wrap things up as follows. Since the final path was obtained uniformly from , we have an element

and we can then unfix to obtain the desired element

I slightly abused -notation in the argument above but the idea was only to give a hint how the argument could be formalized. In fact, we did not need to worry about this at all. Since is a set, there is at most one path in and thus there is also at most one element in

by function extensionality (§4.9). Therefore, the unique choice principle (§3.9) applies to give the desired element of . In fact, also has exactly one element by function extensionality.

In the end, the classical proof of uniqueness of inverses was sufficient and unambiguous. In fact, the same is true for essentially all similar facts of elementary algebra. This is good for multiple reasons but most importantly this means that doing math in HoTT does not involve getting caught up in elementary stuff like this: you can invoke any time without referencing a particular proof since the proof is unique. There is one important caveat:

It is very important that the carrier type of a group is a set!

I fell into this trap when I asked this MathOverflow question. It is very tempting to think that the loop space is a group for every . This is only true if is a 1-type. Otherwise the carrier of is not necessarily a 0-type, the uniqueness of paths is lost, can have many different proofs, which are all relevant and must not be forgotten!


In conclusion, elementary group theory works fine in HoTT. The general feel is a bit different but it’s more fun than cumbersome to see how the axioms work in relevant mathematics. The same is true for much of elementary algebra and, ultimately, proof relevance is never cumbersome since proofs are almost always unique. It is important to remember that the carrier of an algebraic structure must always be a set for this to work!

In the next installment of HoTT Math, we will continue with elementary field theory which presents an additional difficulty since we must handle the fact that multiplicative inverses do not always exist…


CC0 Originally posted on by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.


Comments