The double category of relations is the locally posetal double category $\smash {\mathsf{Rel}^{\mathsf{dbl}}}$ where
- Objects. The objects of $\mathsf{Rel}^{\mathsf{dbl}}$ are sets.
- Vertical Morphisms. The vertical morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$ are maps of sets $f\colon A\to B$.
- Horizontal Morphisms. The horizontal morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$ are relations $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X$.
- $2$-Morphisms. A $2$-cell
of $\mathsf{Rel}^{\mathsf{dbl}}$ is either non-existent or an inclusion of relations of the form
- Horizontal Identities. The horizontal unit functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor of Definition 6.2.5.2.1.
- Vertical Identities. For each $A\in \text{Obj}\webleft (\mathsf{Rel}^{\mathsf{dbl}}\webright )$, we have
\[ \text{id}^{\mathsf{Rel}^{\mathsf{dbl}}}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{id}_{A}. \]
- Identity $2$-Morphisms. For each horizontal morphism $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, the identity $2$-morphism
of $R$ is the identity inclusion
- Horizontal Composition. The horizontal composition functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor of Definition 6.2.5.3.1.
- Vertical Composition of $1$-Morphisms. For each composable pair $A\smash {\overset {F}{\to }}B\smash {\overset {G}{\to }}C$ of vertical morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. maps of sets, we have
\[ g\mathbin {{\circ }^{\mathsf{Rel}^{\mathsf{dbl}}}}f \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g\circ f. \]
- Vertical Composition of $2$-Morphisms. The vertical composition of $2$-morphisms in $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 6.2.5.4.1.
- Associators. The associators of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 6.2.5.5.1.
- Left Unitors. The left unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 6.2.5.6.1.
- Right Unitors. The right unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 6.2.5.7.1.
