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