A hierarchy of ∞-equivalence relations

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 R on a type A is defined as R(x,y):=\mathbf{1}. The quotient A/R of A modulo the trivial relation is just the propositional truncation.

Example -1 (Prop-valued equivalence relations). A Prop-valued equivalence relation on a type A is simply a binary relation R : A \to{}A\to{}\mathsf{Prop} 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 A 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 A consists of a category for which the type of objects is equal to A, 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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s