Hello and welcome to my talk with the title Coherence via Well-foundedness, Taming Set Quotients in Homotopy Type Theory. My name is Jacob von Römer and I'm presenting joint work with Nikolai Krauss.

While the title of this talk contains scary words like coherence or homotopy type theory, I promise that I will keep the talk fairly accessible and that most parts of the talk actually will be independent of homotopy type theory or even type theory, but instead will be completely agnostic towards the basis or the logical foundation we are working in.

To see that, we can take a look at the outline of the talk and see that we will first discuss a purely graph-theoretic problem.

Afterwards, we will discuss our solution to that problem, which we gave the name Noetherian cycle induction. In the last part of the talk, we will then discuss an application of the Noetherian cycle induction,

which is the definition of free groups in homotopy type theory. Let's look at the graph-theoretic problem that I mentioned. Consider a graph or consider all graphs and consider paths in a graph. Now, if we want to prove a property about paths, one easy way to do this is to use that we can prove the property by induction,

because every path is either empty or it's created by adding another edge to a smaller path. But now, if the property we want to prove doesn't hold or isn't able to, isn't formulatable for all paths,

but just for closed paths, then there's no obvious way to apply induction. So take, for example, the closed path in the graph on the left.

If we take out an edge from the graph, from the path, we don't get a smaller closed path, but we get a path which is not closed anymore. So if we want to prove a property for a closed path, it's not clear how to prove it. And indeed, this is, it's important that this is not trivial, because that actually makes certain areas of graph theory interesting or homotopy theory.

And the endeavor of this talk will be to approach a special case of this problem and then to present applications on homotopy type theory.

To tweak the problem a little bit, let's change the graph a bit and say that we are working not in the most simple of graphs, but we're working in directed graphs and in directed multigraphs. So edges have a source and a target, and we can have multiple edges between two vertices.

And we say that we want to prove a property for every closed zigzag in a graph, where a closed zigzag is something like the path or the zigzag marked red in the graph on the left. It's a cycle where we can choose to either go along edges with their direction or against their direction.

And from now on, I will call those cycles, even if that terminology is a bit different from what might be used from graph theory. And obviously, we can't solve this problem in this generality, but we need to make certain assumptions on the graph.

And the first assumption that we want to make is that the graph is locally confluent. What does that mean? That means that for every span that we can find in the graph, so every vertex and every two outgoing edges, like the ones marked on the left,

for every such span, we can find a way to reconnect those edges. So we, for example here, we could complete the span to a cycle by connecting both the paths to this vertex down here.

So this graph is locally confluent. And the next condition that we need for this graph to hold is that it is notarian or co-well-founded, which just means that whenever we have a path, it has to end somewhere.

There are no paths in the graph that extend indefinitely to the right. For example, there's no way to extend the graph which is marked red on the graph on the left.

What are graphs that actually fulfill those requirements? One example, which is also the example we'll be looking at in the last part of this talk, are the graph of words as they appear in the definition of a free group on a set M,

where the vertices are just words of elements of M, which either appear inverted or non-inverted. And two vertices are connected if one is reducible from the other with one step by just cancelling out two subsequent, two equal subsequent letters with the inverted polarity.

So for example, you could either cancel out M and M-1 here, or you could cancel out M3-1 and M3,

and you would arrive at two different reduced words which you could then reduce further. And this graph is locally confluent because it doesn't matter in which order we apply those reductions. We can always end up with the same completely reduced word.

And it's notarian because there's only finitely many steps we can apply to a word to reduce it. So this is a good example and our prime example for a graph that actually fulfills these requirements. And we will always think of the relation of being a relation of reductions or a greater than relation.

And I will also continue this terminology when I talk about an arbitrary relation, as we will assume it in the rest of this talk.

So how do we solve the problem? How do we formulate an induction principle for these cycles? And I subdivided the steps to arrive at this induction principle into four steps, the first of which will be to lift the relation that we are given on an arbitrary set A

to a new relation on the cycles of A. And in a second step, we will then prove that if the original relation is notarian, then the lifted relation on cycles is notarian as well. Then in a third step, we will show how we can decompose any cycle of the graph of the relation

into a confluent cycle and a smaller cycle according to the lifted relation. And using this decomposition, we can then show the theorem that we call a notarian cycle induction,

which basically states that we can show a property for all cycles by just showing it for the empty cycle, for confluent cycle, and for the merge of two cycles. Okay, let's go on to step one. First, we will not extend the relation on A to cycles, but to lists.

And we will use something which we call the list extension of the relation. So let's start off with the relation, and then we will define a relation on the list of elements of A, which is generated inductively by this one generator.

So that just means that every edge in this list relation consists of choosing an element of the list, like this A, and then replacing it with a sequence of elements which are all smaller than A according to our relation.

So we replace one element by a whole sequence of smaller elements. And now we can show that if the original relation is notarian, then the relation on lists is notarian as well. This is not a completely new result, but it's very similar to a similar definition on multi-sets, which is given by Tobias Nipko.

In the second step, we will then go from lists to cycles.

For example, how do we get from lists to cycles? Let's take a cycle like the one on the slide, and we will define its vertex sequence to be just the list which contains all the vertices of the cycle.

So in this case, just a0, a4, a3, a2, a1. Note that with this definition, we kind of assume that every cycle has a base point. And now we say that a cycle gamma can be reduced to a cycle delta according to the lifted reduction relation.

If we can find the rotation of the target, which we will then call delta prime, such that the list of vertices of the first cycle can be reduced to the list of vertices of this cycle delta prime.

And so we got a relation on cycles, and we can then show that if the original relation was notarian, then the relation on cycles is notarian as well. And that's going to be important in the rest of the talk. If a relation is notarian, then its transitive closure is notarian as well.

So what we can also do is take the transitive closure of the original relation, then lift it to cycles, and then take the transitive closure of that. We will denote this by these two pluses for the two transitive closures that we take. For step 3, we will first observe that for any cycle that we can find in a notarian relation, it's either empty or it contains a span.

Like the one which is marked red on the cycle on the right as well. Why is this? I will not show the full proof, but the intuition is the following.

If all the edges in the cycle were oriented in the same way, then we would have an infinite path and the relation would not be notarian anymore. The theorem states that if our relation is notarian and locally confluent, then any cycle can be written as a

merge of a cycle which is smaller according to the transitive closure construction, which I talked about, and a confluence diamond. Now I put merge into square quotes. What does that mean?

I think it's best shown with this picture. We started out with an arbitrary cycle and now we displayed the cycle as pasting together two different cycles. One of them, the cycle on the left, is a confluence diamond. It's the confluence diamond around the span which starts at A3.

And the cycle on the left, it's a new cycle and it's smaller than the cycle we started out with because A9 and A8 are both smaller than A3.

So what we did is take a cycle and be left with a smaller cycle and a confluence cycle. And that's the core mechanism which is behind the proof of our main result, the main result which we called notarian cycle induction, which states the following. So we are given a notarian and locally confluent relation on the set A and a property P on its cycles.

And now property P has to fulfill four different requirements. The first requirement is the following. P must be stable under rotation of cycles. Like I said, a cycle has some sort of a base point and P should not depend on what the base point of the cycle is. Or put differently, if the cycle is the concatenation of a zigzag alpha and a zigzag gamma, then P

on alpha and gamma should be the same of P where we first go along gamma and then along alpha. The next condition is that P should be stable under merging or pasting of cycles. So if there's two cycles like alpha, gamma and gamma to the minus one beta that share

a common zigzag, then P should also hold for the common outer cycle of these two smaller cycles. Then we need to start the induction somehow, which we do by requiring that the property holds for the empty cycle.

And what we also need to show is that P holds for confluent cycles. In practice, and I will not go into too much detail of this, this is useful because proving the property for any cycle might be hard.

But proving the property for confluent cycles might be much, much easier because the confluent cycle usually will come out of some construction which gives a proof for the local confluence. And so the theorem states that if all these four requirements hold, then P of gamma holds for any cycle gamma.

And this is the point of the talk where I will switch from being in a purely set-theoretic, graph-theoretic, classic setting to a type-theoretic setting.

All the notions that I've used so far can be made constructive. And so it's not a big change from going from this classical setting to a type-theoretic setting. And indeed, the type-theoretic version or the type-theoretic-flavored version of the theorem basically looks almost the same.

We started with an arbitrary type A, and we started with a relation which is now a type family indexed twice over A. And P is now a type family which is indexed over the cycles of the relation. And the rest of the theorem basically looks the same.

So now that we are dived into the world of type theory, I will now give a sketch of one place where we can use this induction theorem. And actually which was our motivation behind finding this induction theorem. And this application is the definition of free groups.

Now we've seen free groups as an example for the graph which is notarian and locally confluent. And the problem which I want to state is that there's two different ways to define free groups in homotopy type theory. So the first one would be the type-theoretic representation of the usual construction that we know from a set-theoretic setting as well.

Which is we take words which I encode as lists of m plus m. Meaning that it's lists where the elements of the lists are either m or they are m to the minus one.

So that's why we have m plus m. And then obviously we have to quotient this type of lists by a relation. And we can say that this relation is also an inductive type. It's inductively generated by the following constructor where the reduction step is exactly what I presented earlier.

Whenever we have two subsequent elements in the list that are inverse of each other, then we can cancel them out. But then in homotopy type theory there's also a very convenient way of avoiding having to define this relation.

Which is using the higher groupoid structure of the types themselves. And we can do that by defining the free group instead of the loop space as the loop space of a higher inductive type. So we can define the free group.

And this is the more accepted, the more recognized definition. Is that we take the following higher inductive type which is just one point constructor star. And for every element in m it's got a loop from star to itself. We can also, we could also display this as a homotopy co-equalizer.

But yeah, that's the higher inductive type. And then if we take the loops of this higher inductive type, we basically get the relation for free. Because the relation already holds in the algebra of equalities in homotopy type theory.

And so now we have these two approaches. One which comes from the classic definition and one which comes from synthetic homotopy theory. And we might ask ourselves, and this is an open problem, do these two definitions coincide? In the sense that this quotient on lists is the same as the loop space of the higher inductive type.

And this question remains open. But what we can apply our induction theorem to is an approximation to this open question. Which asks if the two 1-truncations of, the 1-truncations of these two types actually coincide. And because the quotient on the list is already a set, this question is tantamount to asking

is the fundamental group of the free group trivial? Which is a question which might sound odd to people who are not familiar with homotopy type theory. But answering this question, whether the 1-truncations of these two types coincide.

We need to construct an equivalence between two types. And that means that we have to map, we have to construct a map from the quotient of the lists to the 1-truncation of the loop space. And there's a, we have looked at what that means, mapping out of a set quotient into a 1-truncation.

And one can come up with a characterization of the maps. And one possible characterization is that the maps from the quotient into the 1-truncation

are equivalently given by triples consisting of data F, H, and C. Where F is a map from the non-quotiented type into the same codomain. H makes sure that the relation that we quotient by is actually respected.

So whenever L1 reduces to L2, F of L1 equals F of L2. But then because we're not mapping into a set but into a 1-type, we need a third piece of data, which is what we call C for coherence. Which says that any cycle in the graph which comes from the relation that we're quotienting by

has to be mapped to the reflexivity witness. For any cycle of this relation, for any cycle gamma. And so we can just plug in this condition for coherence. We can just plug this in as the P that we have for the induction theorem.

And so that makes it possible, and then I will not go into much detail, to not prove this for an arbitrary gamma anymore but just for confluence cycles. Proving that the other conditions like the rotation and the merge conditions are fulfilled is quite easy in that case.

Okay, so that's one place where we can use Notarian cycle induction. To come to a close with this talk, what are the conclusions? We found a neat way to tackle proofs about cycles, be it in homotopy type theory or in very special settings of graph theory.

And we used this way and this Notarian cycle induction to solve approximations to open problems or to make proofs of these approximations more clean.

And what I haven't mentioned so far is that we have formalized all the contents of this talk and of the paper in the Lean theorem prover with about 1600 lines of codes. And this is not a sealed and done project, but instead we are exploring applicability to other open problems in homotopy type theory.

And right now we are looking a bit into what connections our approach has to problems that appear in the field of higher dimensional rewriting. And at this point I want to say thank you to Vincent van Oostrom who wrote us

a long email explaining to us how our terminology and our approach relates to the problems they face. And as a last point, I want to mention that I am actually currently looking for a job and I would be happy to hear about potential postdoc openings.

Thank you for listening and I hope to see you all in the Q&A session. Goodbye!