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 8.3.5.2.1.
-
•
Vertical Identities. For each $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Rel}^{\mathsf{dbl}}\webright )$, we have
\[ \operatorname {\mathrm{id}}^{\mathsf{Rel}^{\mathsf{dbl}}}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{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 8.3.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 8.3.5.4.1.
-
•
Associators. The associators of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 8.3.5.5.1.
-
•
Left Unitors. The left unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 8.3.5.6.1.
-
•
Right Unitors. The right unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 8.3.5.7.1.
