The Clowder Project

The category $\mathbf{Rel}\webleft (A,B\webright )$ admits a right 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 Right Skew Monoidal Product. The right $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.5.1.1.1.

• The Right 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.5.2.1.1.

• The Right Skew Associators. The natural transformation

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

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

  of Definition 5.5.4.1.1.

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

  of Definition 5.5.5.1.1.