The vertical composition in $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as follows: for each vertically composable pair
of $\alpha $ and $\beta $ as the inclusion of relations
Footnotes
[1] 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 )$;
- We have $a\sim _{R}x$;
- 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 )$.
