Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation from $A$ to $B$.
The following conditions are equivalent:
The relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is an equivalence in $\boldsymbol {\mathsf{Rel}}$, i.e.:
The relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is an isomorphism in $\mathrm{Rel}$, i.e.:
There exists a bijection $f\colon A\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }B$ with $R=\operatorname {\mathrm{Gr}}\webleft (f\webright )$.
We claim that Item 1, Item 2, and Item 3 are indeed equivalent:
Item 1$\iff $Item 2: This follows from the fact that $\boldsymbol {\mathsf{Rel}}$ is locally posetal, so that natural isomorphisms and equalities of $1$-morphisms in $\boldsymbol {\mathsf{Rel}}$ coincide.
Item 2$\implies $Item 3: The equalities in Item 2 imply $R\dashv R^{-1}$, and thus by Proposition 8.4.3.1.1, there exists a function $f_{R}\colon A\to B$ associated to $R$, where, for each $a\in A$, the image $f_{R}\webleft (a\webright )$ of $a$ by $f_{R}$ is the unique element of $R\webleft (a\webright )$, which implies $R=\operatorname {\mathrm{Gr}}\webleft (f_{R}\webright )$ in particular. Furthermore, we have $R^{-1}=f^{-1}_{R}$ (as in Chapter 9: Constructions With Relations, 
). The conditions from Item 2 then become the following:
All that is left is to show then is that $f_{R}$ is a bijection:
The Function $f_{R}$ Is Injective. Let $a,b\in A$ and suppose that $f_{R}\webleft (a\webright )=f_{R}\webleft (b\webright )$. Since $a\sim _{R}f_{R}\webleft (a\webright )$ and $f_{R}\webleft (a\webright )=f_{R}\webleft (b\webright )\sim _{R^{-1}}b$, the condition $f^{-1}_{R}\mathbin {\diamond }f_{R}=\chi _{A}$ implies that $a=b$, showing $f_{R}$ to be injective.
The Function $f_{R}$ Is Surjective. Let $b\in B$. Applying the condition $f_{R}\mathbin {\diamond }f^{-1}_{R}=\chi _{B}$ to $\webleft (b,b\webright )$, it follows that there exists some $a\in A$ such that $f^{-1}_{R}\webleft (b\webright )=a$ and $f_{R}\webleft (a\webright )=b$. This shows $f_{R}$ to be surjective.
Item 3$\implies $Item 2: By Chapter 9: Constructions With Relations, of , we have an adjunction $\operatorname {\mathrm{Gr}}\webleft (f\webright )\dashv f^{-1}$, giving inclusions
We claim the reverse inclusions are also true:
$f^{-1}\mathbin {\diamond }\operatorname {\mathrm{Gr}}\webleft (f\webright )\subset \chi _{A}$: This is equivalent to the statement that if $f\webleft (a\webright )=b$ and $f^{-1}\webleft (b\webright )=a'$, then $a=a'$, which follows from the injectivity of $f$.
$\chi _{B}\subset \operatorname {\mathrm{Gr}}\webleft (f\webright )\mathbin {\diamond }f^{-1}$: This is equivalent to the statement that given $b\in B$ there exists some $a\in A$ such that $f^{-1}\webleft (b\webright )=a$ and $f\webleft (a\webright )=b$, which follows from the surjectivity of $f$.
This finishes the proof.
