5.5.5 The Right Skew Right Unitors

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

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

as in the diagram

whose component

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

at $S$ is given by

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

where $\epsilon \colon J^{*}\circ \text{Ran}_{J}\Longrightarrow \text{id}_{\mathbf{Rel}\webleft (A,B\webright )}$ is the counit 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: