
Topics
 Type Theory
HoTT Math 3: Unit group of a ring
In this installment of HoTT Math, we are taking one more step toward elementary field theory by exploring the unit group of a ring.
A commutative (unital) ring is a set with two constants , one unary operation , two binary operations along with the usual axioms: , ,
and
Commutativity of addition can be derived as usual using the fact that
If you want to test your path manipulation skills, you can try to write down the resulting term for
However, as we discussed last time, this is not necessary since the proof is ultimately not relevant when the carrier of an algebra is a set.
Reading off the usual definition of unit, we obtain the type
Elements of type are pairs , where and . Because is a set and inverses are unique, there is always at most one such , which means that is a proposition. Therefore, we can comprehend the set of units:
(Subset comprehension is discussed in §3.5 of the book.) Technically, elements of are triples where and . Thus is not merely a subset of but each element of comes equipped with a justification for being in . Since for each there is at most one , we can identify the two without much confusion but the extra coordinates are actually helpful for proving things about .
To illustrate this, let’s outline the verification that is a group under multiplication. We will view elements of as pairs but we will forget the path witnessing that . Since we’re working with sets, we shouldn’t worry about paths anyway.1 To begin, we need to isolate the group operations:

First, we see that since we have a path by the identity axiom; this will be our group identity.

Next, we see that if then . Indeed, if and then
From this, we directly extract our group multiplication .

Finally, we see that if then . (This is immediate from commutativity but a slightly longer argument shows that this works even without this assumption.) As a result, we get the group inverse .
To conclude the argument, it suffices to verify that is inhabited. Associativity and identity are immediate consequences of . The tacit path coordinates are handy for inverses: the path simply consists of the two implied paths and !
The key difference between this proof and the classical proof that is a group is the way we used the definition of . At each step of the classical proof, we need to invoke the definition of to get the relevant inverses, do the same computations, and then forget the extra information. In the proofrelevant argument, the subset incorporates its definition and the relevant inverses are already there to be used in computations. To keep the argument from involving too many (ultimately irrelevant) path computations, we still forgot one piece of the definition of in the outline above. This kind of selective unraveling can be useful since formal definitions can rapidly become unwieldy. We did end up invoking the path coordinates at the very end to verify the identity axiom. However, we didn’t really need the paths themselves, we just needed to remember that elements aren’t arbitrary pairs, they are pairs such that . This is what the seemingly irrelevant path coordinate does, the relevant data is not the path itself, it is the type of the path that matters.
The lesson is that while proofrelevant mathematics does force you to carry extra baggage, that baggage is actually handy. Moreover, you can always manage the burden by selectively unraveling the contents of the baggage. In fact, you also carry this baggage when doing classical mathematics except that you conceal the baggage in your memory, recalling each item as you need it. The problem with this strategy is that it’s easy to forget things if you are not careful. Proofrelevant mathematics forces you to keep track of everything!
Post Scriptum
In the comments, Toby Bartels pointed out that the argument above contains a major typetheoretic faux pas: using type declarations as propositions. The cause of this is the deliberate omission of the path coordinate which leads to phrases like “we see that since […]” and “we see that if then .” The problem is that type declarations are either correct or not (and this is decidable!) but not true or false. Indeed, true and false are both values that can be used but correct and incorrect are not — there is no value in being incorrect! This may seem like a subtle difference but it is actually a very important one in type theory since there is little other separation of syntax and semantics.
Below, I produced three more variants of the above argument that avoid the trouble with Version 0 above. The first is simply does not omit the path coordinates. The second uses the membership relation where the original used an erroneous type declaration. The third is a direct translation of the classical proof, also using the membership relation. To facilitate comparison, I tried to keep the three versions as close as possible to the original. I am curious to know which of the four versions you prefer, or if you have yet another version that you prefer!
Version 1. Let’s outline the verification that is a group under multiplication. To begin, we need to isolate the group operations:

First, is our group identity where is an instance of the identity axiom.

Next, the group product is defined by , where

Finally, group inverses are defined by , where (A slightly longer argument shows that this works even without the commutativity assumption.)
To conclude the argument, it suffices to verify that is inhabited. Associativity and identity are immediate consequences of . The path is composed of , , and the paths must match since is a set.
Version 2. Let’s outline the verification that is a group under multiplication. By virtue of univalence, there are multiple ways to look at . Instead of viewing it as a subset of we can also view it as a subset of , namely
Thus denotes the proposition It turns out that this view of will be easier to work with. To begin, we need to isolate the group operations:

First, we see that since we have a path by the identity axiom; this will be our group identity.

Next, we see that if then too. Indeed, if and then
From this, we directly extract our group multiplication .

Finally, we see that if then since implies by commutativity. (A slightly longer argument shows that this works even for noncommutative rings.) As a result, we get the group inverse .
To conclude the argument, it suffices to verify that is inhabited. Associativity and identity are immediate consequences of . The path is composed of and , which hold because .
Version 3. Let’s outline the verification that is a group under multiplication. Per definition of , we will write to mean . To begin, we need to isolate the group operations:

First, we see that since by the identity axiom; this will be our group identity.

Next, we see that if then too. Indeed, since and there are such that and Then
which shows that Thus our group multiplication is (the restriction of) the usual ring multiplication.

Finally, we see that if then, by definition of the proposition , there is a unique such that . By commutativity, which means that and this is the group inverse of .
To conclude the argument, it suffices to verify that is inhabited. Associativity and identity are immediate consequences of . The remaining identity follows immediately from the definition of group inverses.
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

François G. Dorais wrote
In the definition of units, I chose to use right inverses instead of left inverses. This makes no difference since the ring is commutative. In fact, this makes no difference even if the ring is not commutative. If we use the left inverse definition
we realize that the group of units is actually the exact same as the one above: they both equal
by univalence! The proof that this is a group is actually the same seen from the left or from the right. (Note that the verification that left and right inverses are the same is the main content of the definition of the group inverse.)
I guess there is a side lesson here: univalence applies to proofs too! In HoTT, what we used to call “symmetric arguments” are actually the exactly the same…

Toby Bartels wrote
I don’t like to see typing declarations used as if they were propositions. To some extent they are; a term may or may not have a certain type. But it’s an important feature of intensional type theory that this question is decidable (and, usually, immediately so); you can see from the form of the term whether it has the claimed type or not. But when you abbreviate (x, y, p) as (x, y), then this is no longer decidable (which would solve the word problem for rings).
This is where type theorists (at least those who use the colon for typing declarations) use the set membership symbol ‘∈’, with the benefit that we actually have a proposition internal to the type theory (rather than merely the external proposition that a term has a given type). Although you defined the set of units of R as a subset of R, it can also be realised as a subset of R × R, and that is how you are using it. In general, given any set S, any subset A of S, and any element e of S, there is a mere proposition e ∈ A (with a subscript S on the ‘∈’ to be most proper) that indicates that e belongs to A (which I’m sure is defined somewhere in the HoTT book and which you can probably write down for yourself).

François G. Dorais replied to Toby Bartels
You’re right but the point I’m trying to make is that there is a right balance for doing things informally, which is actually in between forgetting everything (the fully extensional way) and remembering everything (the fully intensional way).
If I work the fully intensional way, then I need to do something with the paths all the time. If I think of elements of as triples then the group product is
and I am compelled to write it that way (perhaps relying on my proof assistant to write the messy path for me). That’s an unnecessary burden since the path is always uniquely determined and almost never used.
If I work the fully extensional way, then I need to recall all the necessary data all the time. That’s also an unnecessary burden. We’re all used to it but anyone who spent time teaching intro to proofs at the college level knows how hard it is to communicate the idea of “using definitions”…
The middle ground I used seems just right to me: all the data I need is right there and the data I don’t need to worry about is out of sight. Note that I still remember the extra data is there, I just choose to ignore it since I know in advance that I don’t need to worry about it.

François G. Dorais replied to Toby Bartels
Regarding your alternative of using the relation. I’m not too fond of that. In this case, the relation takes to . You need to remember how is defined to figure out what actually means. That’s just a sneaky way of mapping proofirrelevant mathematics into proofrelevant mathematics. There is no point in doing proofrelevant mathematics if it’s done that way. I do see your point that one way to formalize my inbetween solution is to have map to . That’s neat but there is nothing there to suggest that I had an a priori reason for doing that.

François G. Dorais replied to Toby Bartels
Actually, since I also had to explain my a priori reason for dropping the path component, there may be more merit to using than I thought. It is a more explicit way of forgetting the path coordinate without contaminating the intensional theory with bits of extensionality.
I’m still not feeling great about this. The relation is just a kludge to eliminate the set builder notation – is defined as – and the set builder notation is already something I was trying to avoid. More importantly, there is also the temptation to use it to forget things that are actually useful…

François G. Dorais replied to Toby Bartels
I added a note explaining this. You’re completely right about this but I still have a hard time with it. This is magnified by another problem I was dealing with: to find a good way to handle partial functions. The confounding thing is that a partial function is actually equal to its domain of definition , what’s even more confusing is that is also equal to ! Most of the time, I think that’s pretty neat, but it also gives me some bad headaches…

François G. Dorais replied to Toby Bartels
After thinking about this some more, I decided to actually write out three variants of the proof, one spelling out the paths, another using , and a third using (which is really just the classical proof recast in HoTT). I will insert these at the end of the post when I’m done typing them so that I can compare all three and see the pros and cons of each.

François G. Dorais wrote
My favorite is Version 1. My main problem is that it was harder to write since I wanted to minimize the effect of the paths. I also hated wasting valuable letters to name these paths. This is probably just me, but it was hard to resist computing the paths in my head as I was composing the proof. Summary: this is fantastic for reading, but not for writing.
Currently, Version 0 and Version 2 are tied for second place. The basic arguments are identical, so there is no distinction there. Version 2 does correct the error of Version 0, but it introduces a new one. In the end, writing is technically incorrect. The operation is on , not on . One could argue that the same error is in Version 0, but there abbreviates , so this usage is consistent with the local conventions. The other drawback of Version 2 is that the group operations are defined by specifying each individual value, I prefer the expressions in Version 0.

Toby Bartels replied to François G. Dorais
Version 1 really gives the flavour of fully proofrelevant mathematics, albeit at the cost of ultimately irrelevant verbiage. I wonder if you might rewrite ‘A slightly longer argument shows that this works even without the commutativity assumption.’ as ‘A slightly longer construction of q shows that this works even without the commutativity assumption.’ in that version. (That sentence was also left out of Version 3, I assume accidentally.)