The ($2$-)category of relations is self-dual:
-
1.
Self-Duality I. We have an isomorphism
\[ \mathrm{Rel}^{\mathsf{op}}\mathrel {\smash {\overset {\scriptscriptstyle \text{eq.}}\cong }}\mathrm{Rel} \]of categories.
-
2.
Self-Duality II. We have a $2$-isomorphism
\[ \boldsymbol {\mathsf{Rel}}^{\mathsf{op}}\mathrel {\smash {\overset {\scriptscriptstyle \text{eq.}}\cong }}\boldsymbol {\mathsf{Rel}} \]of $2$-categories.
-
•
Bijective on objects, which is clear.
-
•
Bijective on $1$-morphisms, which was shown in Item 1.
-
•
Bijective on $2$-morphisms, which follows from Chapter 9: Constructions With Relations,
of .
8.4.1 Self-Duality
Proof of Proposition 8.4.1.1.1.
Item 1: Self-Duality I
We claim that the functor
\[ F\colon \mathsf{Rel}^{\mathsf{op}}\to \mathsf{Rel} \]
given by the identity on objects and by $R\mapsto R^{\dagger }$ on morphisms is an isomorphism of categories.
By Chapter 11: Categories, Item 1 of Proposition 11.6.8.1.3, it suffices to show that $F$ is bijective on objects (which is clear) and fully faithful. Indeed, the map
\[ \webleft (-\webright )^{\dagger }\colon \mathrm{Rel}\webleft (A,B\webright )\to \mathrm{Rel}\webleft (B,A\webright ) \]
defined by the assignment $R\mapsto R^{\dagger }$ is a bijection by Chapter 9: Constructions With Relations, of , showing $F$ to be fully faithful.
Item 2: Self-Duality II
We claim that the $2$-functor
\[ F\colon \mathsf{Rel}^{\mathsf{op}}\to \mathsf{Rel} \]
given by the identity on objects, by $R\mapsto R^{\dagger }$ on morphisms, and by preserving inclusions on $2$-morphisms via Chapter 9: Constructions With Relations, of , is an isomorphism of categories.
By , of , it suffices to show that $F$ is:
Thus $F$ is indeed a $2$-isomorphism of categories.
