Definition 6.2.5.4.1 (00KN): The Vertical Composition of 2-Morphisms in $\mathsf{Rel}^{\mathsf{dbl}}$

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 vertical composition in $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as follows: for each vertically composable pair

of $2$-morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. for each each pair

of inclusions of relations, we define the vertical composition

of $\alpha $ and $\beta $ as the inclusion of relations

given by the pasting of inclusions¹

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

We have $h\webleft (f\webleft (a\webright )\webright )\sim _{T}k\webleft (g\webleft (x\webright )\webright )$;

is implied by the statement

since

If $a\sim _{R}x$, then $f\webleft (a\webright )\sim _{S}g\webleft (x\webright )$, as $S\circ \webleft (f\times g\webright )\subset R$;
If $b\sim _{S}y$, then $h\webleft (b\webright )\sim _{T}k\webleft (y\webright )$, as $T\circ \webleft (h\times k\webright )\subset S$, and thus, in particular:
- If $f\webleft (a\webright )\sim _{S}g\webleft (x\webright )$, then $h\webleft (f\webleft (a\webright )\webright )\sim _{T}k\webleft (g\webleft (x\webright )\webright )$.