Suppose you have come up with a certain extra structure, formulated in homotopy type theory, that a binary type-valued relation on may possess, and you’d like to say that it is an ∞-equivalence relation. Well, then you have to show that it is one! In this post I’d like to give a suggestion of how you might go about it.
Presumably, any relation which possesses the extra structure of your notion of an equivalence relation is going to be at least reflexive in an obvious way. So, we suppose you’ve got a structure which takes a reflexive relation on and returns the structure you’ve come up with.
The key to knowing whether is any good, is to compare it with the surjective maps that go out from . After all, at some point you will define a suitable quotient type together with a surjective quotient map . Let us write for the type of all surjective maps out of into some small type, i.e.
Recall that is defined as .
To any map , not necessarily a surjective one, we can associate a reflexive relation on , by substituting in the identity type on . More precisely, we define a map , by taking to be the reflexive relation on consisting of the binary relation and the proof of reflexivity. We might call the `pre-kernel’ of , since morally it is the kernel but it lacks an explicit structure of an equivalence relation. For all we know, it might possess this structure in many different ways. There are two things that need to be done:
Lift the pre-kernel. The first thing you need to do is to lift to an operation as indicated in the diagram
In other words, every pre-kernel needs to be given the structure of an equivalence relation so that it becomes a kernel.
Find an inverse to the kernel operation. Second, you need to show that is an equivalence.
Just to spell out what the second requirement means, it involves finding for every equivalence relation on , the quotient and a surjective map . This gives the inverse of . Then, to show that , you need to show that there is a commuting triangle
in which the bottom map is an equivalence. Finally, the quotenting operation needs to be shown effective, i.e. it needs to be shown that . This involves first showing that, for any equivalence relation there is a fiberwise equivalence
preserving reflexivity. This determines a path . To complete the proof of effectiveness, it needs to be shown that . In other words, that the canonical structure of being an equivalence relation that the pre-kernel possesses, agrees with the assumed structure , that is an equivalence relation.
There are already at least two notions of ∞-equivalence relations that satisfy the two requirements that I described above:
- The first one is completely uninformative, but it is out there anyway. We can take to be just . Since for any map, the total space of the fibers is equivalent to the domain, this satisfies the two requirements for completely general reasons. We learned nothing from this example.
- The second example is that of `principal equivalence relations’. I hope to write about them soon. For now, I will just mentioned that I’ve given a presentation about them at the Workshop on Univalent Foundations and Categorical Logic, in Leeds. If you are curious you can already have a look at my slides.
Neither of these examples is completely satisfactory though. In both cases, the types is a large type, and we need the univalence axiom to extend to . I believe that ultimately, the type should be a small type of which the formulation does not rely on the univalence axiom, and for which can be lifted to without univalence. Moreover, in the scenario where that is possible it would be nice that the assertion that is an equivalence for each type , is itself equivalent to the univalence axiom. I hope that something like that would be possible in the future.