For each horizontal morphism $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, the component
-
1This is justified by Chapter 9: Constructions With Relations,
of .
8.3.5.6 The Left Unitors
