We have seen what kind of structure the structure of an ∞-equivalence relation is. Now it is time to describe some classes of examples. Of course, once you’ve shown that your notion of equivalence relation meets the two requirements, then you have an exhaustive class of examples: the kernels of maps. Nevertheless, there are some classes of examples that naturally come up in a different way, and we want to make sure they are included.
Example -2 (The trivial relation). The trivial relation relates everything in a unique way. More precisely, the trivial relation on a type is defined as . The quotient of modulo the trivial relation is just the propositional truncation.
Example -1 (Prop-valued equivalence relations). A Prop-valued equivalence relation on a type is simply a binary relation which is reflexive, symmetric and transitive in the usual sense. Since the relation takes values in the (small) mere propositions, we don’t need to impose any further conditions. The quotient operation for Prop-valued equivalence relations is the set-quotient (although, the set-quotients are usually only called so if the underlying type is also a set, but this doesn’t matter at all).
Example 0 (Pre-1-groupoid structure). A pre-1-groupoid structure on a type consists of a category for which the type of objects is equal to , and in which every morphism is invertible. A pre-1-groupoid can be made into a 1-groupoid by `Rezk-completing’ it. This process is described in detail in Chapter 9 of the HoTT book.
Given a notion of ∞-equivalence relation, the ‘pre-n-groupoid structures’ should correspond precisely to the ∞-equivalence relations taking values in the subuniverse of (n-1)-truncated types. Moreover, quotienting operation for the ∞-equivalence relations should correspond to the quotienting operation for pre-n-groupoid structures, while it is completely indifferent about truncation levels. Luckily, it is not too hard to imagine how that would go. Note that in each case (both the finite truncation levels and the unrestricted level), the quotienting operation is a version of Rezk-completion. More precisely, the quotient is the image of (the action on objects of) the Yoneda-embedding.