The vertical composition in $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as follows: for each vertically composable pair
8.3.5.4 Vertical Composition of 2-Morphisms
Proof of the Inclusion in Definition 8.3.5.4.1.
The inclusion
\[ T\circ [(h\circ f)\times (k\circ g)]\subset R \]
follows from the fact that, given $(a,x)\in A\times X$, the statement
-
•
We have $h(f(a))\sim _{T}k(g(x))$;
is implied by the statement
-
•
We have $a\sim _{R}x$;
since
-
•
If $a\sim _{R}x$, then $f(a)\sim _{S}g(x)$, as $S\circ (f\times g)\subset R$;
-
•
If $b\sim _{S}y$, then $h(b)\sim _{T}k(y)$, as $T\circ (h\times k)\subset S$, and thus, in particular:
-
•
If $f(a)\sim _{S}g(x)$, then $h(f(a))\sim _{T}k(g(x))$.
-
•
This finishes the proof.
