# 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

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 $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.