The Clowder Project

The category $\mathbf{Rel}\webleft (A,B\webright )$ admits a left skew monoidal category structure consisting of

• The Underlying Category. The posetal category associated to the poset $\mathbf{Rel}\webleft (A,B\webright )$ of relations from $A$ to $B$ of Item 2 of Definition 5.1.1.1.3.
• The Left Skew Monoidal Product. The left $J$-skew monoidal product
  \[ \lhd _{J}\colon \mathbf{Rel}\webleft (A,B\webright )\times \mathbf{Rel}\webleft (A,B\webright )\to \mathbf{Rel}\webleft (A,B\webright ) \]

  of Definition 5.4.1.1.1.

• The Left Skew Monoidal Unit. The functor
  \[ \mathbb {1}^{\mathbf{Rel}\webleft (A,B\webright ),\lhd _{J}} \colon \mathsf{pt}\to \mathbf{Rel}\webleft (A,B\webright ) \]

  of Definition 5.4.2.1.1.

• The Left Skew Associators. The natural transformation

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

  of Definition 5.4.3.1.1.
• The Left Skew Left Unitors. 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 )} \]

  of Definition 5.4.4.1.1.

• The Left Skew Right Unitors. 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 )} \]

  of Definition 5.4.5.1.1.