For each horizontal morphism $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, the component

of the left unitor of $\mathsf{Rel}^{\mathsf{dbl}}$ at $R$ is the identity inclusion[1]


Footnotes


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: