6.5.4 The Right Skew Left Unitors

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

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

as in the diagram

whose component

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

at $R$ is given by the composition

\begin{align*} R & \mkern 10mu\mathrlap {\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}}\mkern 50mu \chi _{B}\mathbin {\diamond }R\\ & \mkern 10mu\mathrlap {\mathbin {\overset {\eta _{\chi _{B}}}{\Longrightarrow }}\mathbin {\diamond }\text{id}_{R}}\mkern 50mu \text{Ran}_{J}\webleft (J^{*}\webleft (\chi _{A}\webright )\webright )\mathbin {\diamond }R\\ & \mkern 10mu\mathrlap {\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}}\mkern 50mu \text{Ran}_{J}\webleft (J^{*}\mathbin {\diamond }\chi _{A}\webright )\mathbin {\diamond }R\\ & \mkern 10mu\mathrlap {\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}}\mkern 50mu \text{Ran}_{J}\webleft (J\webright )\mathbin {\diamond }R\\ & \mkern 10mu\mathrlap {\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}}\mkern 50mu R\rhd _{J}J, \end{align*}

where $\eta \colon \text{id}_{\mathbf{Rel}\webleft (B,B\webright )}\Longrightarrow \text{Ran}_{J}\circ J^{*}$ is the unit of the adjunction $J^{*}\dashv \text{Ran}_{J}$.


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


You can also use the contact form below: