The 2-/category of relations is self-dual:
-
1.
Self-Duality I. We have an isomorphism
\[ \mathsf{Rel}^{\mathsf{op}}\cong \mathsf{Rel} \]of categories.
-
2.
Self-Duality II. We have a 2-isomorphism
\[ \boldsymbol {\mathsf{Rel}}^{\mathsf{op}}\cong \boldsymbol {\mathsf{Rel}} \]of 2-categories.
-
•
Bijective on objects, which follows by definition.
-
•
Bijective on $1$-morphisms, which was shown in Item 1.
-
•
Bijective on 2-morphisms, which follows from Item 1 of Proposition 8.1.5.1.3.
8.5.1 Self-Duality
Proof of Proposition 8.5.1.1.1.
Item 1: Self-Duality I
We claim that the functor
\[ (-)^{\dagger }\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. Note that this is indeed a functor by Item 3 and Item 6 of Proposition 8.1.5.1.3.
By Chapter 11: Categories, Item 1 of Proposition 11.6.8.1.3, it suffices to show that $(-)^{\dagger }$ is bijective on objects (which follows by definition) and fully faithful. Indeed, the map
\[ (-)^{\dagger }\colon \mathrm{Rel}(A,B)\to \mathrm{Rel}(B,A) \]
defined by the assignment $R\mapsto R^{\dagger }$ is a bijection by Item 5 of Proposition 8.1.5.1.3, showing $(-)^{\dagger }$ to be fully faithful.
Item 2: Self-Duality II
We claim that the 2-functor
\[ (-)^{\dagger }\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 Item 1 of Proposition 8.1.5.1.3, is an isomorphism of categories.
By 
, it suffices to show that $(-)^{\dagger }$ is:
Thus $(-)^{\dagger }$ is indeed a 2-isomorphism of categories.
