What kind of structure is the structure of an ∞-equivalence relation?

Suppose you have come up with a certain extra structure, formulated in homotopy type theory, that a binary type-valued relation R on A 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 \mathsf{isEqRel}_A(R,\rho) which takes a reflexive relation (R,\rho) on A and returns the structure you’ve come up with.

The key to knowing whether \mathsf{isEqRel}_A is any good, is to compare it with the surjective maps that go out from A. After all, at some point you will define a suitable quotient type A/R together with a surjective quotient map q_R : A\to{}A/R. Let us write (A \mathbin{\downarrow{}}_s U) for the type of all surjective maps out of A into some small type, i.e.

(A \mathbin{\downarrow{}}_s U) := \Sigma_{(B:U)}\Sigma_{(f:A\to{} B)}~\mathsf{isSurj}(f).

Recall that \mathsf{isSurj}(f) is defined as \Pi_{(b:B)}~\|\mathsf{fib}_f(b)\|.

To any map f : A\to{} B, not necessarily a surjective one, we can associate a reflexive relation on A, by substituting f in the identity type on B. More precisely, we define a map k_A :(A \mathbin{\downarrow{}}_s U) \to{} \mathsf{rRel}(A), by taking k_A(f) to be the reflexive relation on A consisting of the binary relation x,y \mapsto{} (f(x)=f(y)) and the proof x \mapsto \mathsf{refl}_{f(x)} of reflexivity. We might call k_A(f) the `pre-kernel’ of f, 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 k_A to an operation K_A as indicated in the diagram

20161009_1In 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 K_A is an equivalence.

Just to spell out what the second requirement means, it involves finding for every equivalence relation \mathcal{R} on A, the quotient A/\mathcal{R} and a surjective map q_{\mathcal{R}} : A\to A/\mathcal{R}. This gives the inverse Q_A of K_A. Then, to show that Q_A\circ K_A=1, you need to show that there is a commuting triangle


in which the bottom map is an equivalence. Finally, the quotenting operation Q_A needs to be shown effective, i.e. it needs to be shown that K_A\circ Q_A =1. This involves first showing that, for any equivalence relation \mathcal{R}:=(R,\rho,H) there is a fiberwise equivalence

\Pi_{(x,y:A)} (q_R(x)=q_R(y)) \to{} R(x,y)

preserving reflexivity. This determines a path p : k_A(q_{\mathcal{R}})=(R,\rho). To complete the proof of effectiveness, it needs to be shown that \mathsf{trans}(p,\mathsf{pr}_2(K_A(Q_A(\mathcal{R})))= H. In other words, that the canonical structure of being an equivalence relation that the pre-kernel k_A(Q_A(\mathcal{R})) possesses, agrees with the assumed structure H, that (R,\rho) is an equivalence relation.

There are already at least two notions of ∞-equivalence relations that satisfy the two requirements that I described above:

  1. The first one is completely uninformative, but it is out there anyway. We can take \mathsf{isEqRel}_A to be just \mathsf{fib}_{k_A}. 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.
  2. 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 \mathsf{isEqRel}_A(R,\rho) is a large type, and we need the univalence axiom to extend k_A to K_A. I believe that ultimately, the type \mathsf{isEqRel}_A(R,\rho) should be a small type of which the formulation does not rely on the univalence axiom, and for which k_A can be lifted to K_A without univalence. Moreover, in the scenario where that is possible it would be nice that the assertion that K_A is an equivalence for each type A, is itself equivalent to the univalence axiom. I hope that something like that would be possible in the future.


One thought on “What kind of structure is the structure of an ∞-equivalence relation?

  1. Pingback: A hierarchy of ∞-equivalence relations | Egbert RIJKE

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