The horizontal composition functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor
\[ \mathbin {\odot }^{\mathsf{Rel}^{\mathsf{dbl}}} \colon \mathsf{Rel}^{\mathsf{dbl}}_{1}\operatorname*{\mathbin {\times }}_{\mathsf{Rel}^{\mathsf{dbl}}_{0}}\mathsf{Rel}^{\mathsf{dbl}}_{1} \to \mathsf{Rel}^{\mathsf{dbl}}_{1} \]
of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor where
-
•
Action on Objects. For each composable pair $\smash {A\mathbin {\overset {R}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}B\mathbin {\overset {S}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}C}$ of horizontal morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, we have
\[ S\mathbin {\odot }R\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S\mathbin {\diamond }R, \]where $S\mathbin {\diamond }R$ is the composition of $R$ and $S$ of Definition 8.1.3.1.1.
-
•
Action on Morphisms. For each horizontally composable pair
of 2-morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. for each pair
of inclusions of relations, the horizontal composition
of $\alpha $ and $\beta $ is the inclusion of relations
