6.4.4 The Left Skew Left Unitors

Let $A$ and $B$ be sets and let $J\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.

The left $J$-skew left unitor of $\mathbf{Rel}\webleft (A,B\webright )$ is the natural transformation

\[ \lambda ^{\mathbf{Rel}\webleft (A,B\webright ),\lhd _{J}} \colon {\lhd _{J}}\circ {\webleft ({\mathbb {1}^{\mathbf{Rel}\webleft (A,B\webright )}_{\lhd _{J}}}\times {\mathsf{id}}\webright )} \Longrightarrow \mathbf{\lambda }^{\mathsf{Cats}_{\mathsf{2}}}_{\mathbf{Rel}\webleft (A,B\webright )} \]

as in the diagram

whose component

\[ \lambda ^{\mathbf{Rel}\webleft (A,B\webright ),\lhd _{J}}_{R} \colon \underbrace{J\lhd _{J}R}_{\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}J\mathbin {\diamond }\text{Rift}_{J}\webleft (R\webright )} \hookrightarrow R \]

at $R$ is given by

\[ \lambda ^{\mathbf{Rel}\webleft (A,B\webright ),\lhd _{J}}_{R}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\epsilon _{R}, \]

where $\epsilon \colon J_{*}\mathbin {\diamond }\text{Rift}_{J}\Longrightarrow \text{id}_{\mathbf{Rel}\webleft (A,B\webright )}$ is the counit of the adjunction $J_{*}\dashv \text{Rift}_{J}$.


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


You can also use the contact form below: