Subsubsection 6.2.5.3 (00KK): Horizontal Composition

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 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 Chapter 7: Constructions With Relations, Definition 7.3.12.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¹

¹This is justified by noting that, given $\webleft (a,c\webright )\in A\times C$, the statement

We have $a\sim _{\webleft (U\mathbin {\diamond }T\webright )\circ \webleft (f\times h\webright )}c$, i.e. $f\webleft (a\webright )\sim _{U\mathbin {\diamond }T}h\webleft (c\webright )$, i.e. there exists some $y\in Y$ such that:
1. We have $f\webleft (a\webright )\sim _{T}y$;
2. We have $y\sim _{U}h\webleft (c\webright )$;

is implied by the statement

We have $a\sim _{S\mathbin {\diamond }R}c$, i.e. there exists some $b\in B$ such that:
1. We have $a\sim _{R}b$;
2. We have $b\sim _{S}c$;

since:

If $a\sim _{R}b$, then $f\webleft (a\webright )\sim _{T}g\webleft (b\webright )$, as $T\circ \webleft (f\times g\webright )\subset R$;
If $b\sim _{S}c$, then $g\webleft (b\webright )\sim _{U}h\webleft (c\webright )$, as $U\circ \webleft (g\times h\webright )\subset S$.

The Clowder Project

6.2.5.3 Horizontal Composition