The 2-/category of relations with apartness-composition-is self-dual:
Self-Duality I. We have an isomorphism
of categories.
Self-Duality II. We have a 2-isomorphism
of 2-categories.
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 4 and Item 7 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
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.
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:
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.
Thus $(-)^{\dagger }$ is indeed a 2-isomorphism of categories.
