6.4.5 The Left Skew Right 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 right unitor of $\mathbf{Rel}\webleft (A,B\webright )$ is the natural transformation

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

as in the diagram

whose component

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

at $R$ is given by the composition

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

where $\eta \colon \text{id}_{\mathbf{Rel}\webleft (A,A\webright )}\Longrightarrow \text{Rift}_{J}\circ J_{*}$ is the unit 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: