The Clowder Project

The category $\mathsf{Rel}$ admits a closed symmetric monoidal category structure consisting of^[1]

• The Underlying Category. The category $\mathsf{Rel}$ of sets and relations of Definition 5.2.1.1.1.
• The Monoidal Product. The functor
  \[ \times \colon \mathrm{Rel}\times \mathrm{Rel}\to \mathrm{Rel} \]

  of Definition 5.2.2.1.1.

• The Internal Hom. The internal Hom functor
  \[ \mathbf{Rel}\colon \mathrm{Rel}^{\mathsf{op}}\times \mathrm{Rel}\to \mathrm{Rel} \]

  of Definition 5.2.2.7.1.

• The Monoidal Unit. The functor
  \[ \mathbb {1}^{\mathrm{Rel}} \colon \mathsf{pt}\to \mathrm{Rel} \]

  of Definition 5.2.2.2.1.

• The Associators. The natural isomorphism
  \[ \alpha ^{\mathrm{Rel}} \colon {\times }\circ {\webleft ({\times }\times \text{id}_{\mathrm{Rel}}\webright )} \mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}{\times }\circ {\webleft (\text{id}_{\mathrm{Rel}}\times {\times }\webright )}\circ {\mathbf{\alpha }^{\mathsf{Cats}}_{\mathrm{Rel},\mathrm{Rel},\mathrm{Rel}}} \]

  of Definition 5.2.2.3.1.

• The Left Unitors. The natural isomorphism
  \[ \lambda ^{\mathrm{Rel}}\colon {\times }\circ {\webleft (\mathbb {1}^{\mathrm{Rel}}\times \text{id}_{\mathrm{Rel}}\webright )} \mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}\mathbf{\lambda }^{\mathsf{Cats}_{\mathsf{2}}}_{\mathrm{Rel}} \]

  of Definition 5.2.2.4.1.

• The Right Unitors. The natural isomorphism
  \[ \rho ^{\mathrm{Rel}}\colon {\times }\circ {\webleft ({\mathsf{id}}\times {\mathbb {1}^{\mathrm{Rel}}}\webright )}\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}\mathbf{\rho }^{\mathsf{Cats}_{\mathsf{2}}}_{\mathrm{Rel}} \]

  of Definition 5.2.2.5.1.

• The Symmetry. The natural isomorphism
  \[ \sigma ^{\mathrm{Rel}} \colon {\times } \mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}{\times }\circ {\mathbf{\sigma }^{\mathsf{Cats}_{\mathsf{2}}}_{\mathrm{Rel},\mathrm{Rel}}} \]

  of Definition 5.2.2.6.1.