Proposition 5.3.1.1.1 (00KX): Self-Duality for the (2-)Category of Relations

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

The ($2$-)category of relations is self-dual:

Self-Duality I. We have an isomorphism
\[ \mathrm{Rel}^{\mathsf{op}}\mathrel {\smash {\overset {\scriptscriptstyle \text{eq.}}\cong }}\mathrm{Rel} \]

of categories.
Self-Duality II. We have a $2$-isomorphism
\[ \textbf{Rel}^{\mathsf{op}}\mathrel {\smash {\overset {\scriptscriptstyle \text{eq.}}\cong }}\textbf{Rel} \]

of $2$-categories.

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 8: Categories, Item 1 of Proposition 8.5.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 6: Constructions With Relations, Item 5 of Proposition 6.3.11.1.3, 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 6: Constructions With Relations, Item 1 of Proposition 6.3.11.1.3, is an isomorphism of categories.

By of , it suffices to show that $F$ is:

Bijective on objects, which is clear.
Bijective on $1$-morphisms, which was shown in Item 1.
Bijective on $2$-morphisms, which follows from Chapter 6: Constructions With Relations, Item 1 of Proposition 6.3.11.1.3.

Thus $F$ is indeed a $2$-isomorphism of categories.