6.2.3 The Closed Symmetric Monoidal Category of Relations
6.2.3.1 The Monoidal Product
The monoidal product of $\mathsf{Rel}$ is the functor
\[ \times \colon \mathsf{Rel}\times \mathsf{Rel}\to \mathsf{Rel} \]
where
- Action on Objects. For each $A,B\in \text{Obj}\webleft (\mathsf{Rel}\webright )$, we have
\[ \mathord {\times }\webleft (A,B\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A\times B, \]
where $A\times B$ is the Cartesian product of sets of Chapter 2: Constructions With Sets, 
.
- Action on Morphisms. For each $\webleft (A,C\webright ),\webleft (B,D\webright )\in \text{Obj}\webleft (\mathsf{Rel}\times \mathsf{Rel}\webright )$, the action on morphisms
\[ \times _{\webleft (A,C\webright ),\webleft (B,D\webright )}\colon \mathrm{Rel}\webleft (A,B\webright )\times \mathrm{Rel}\webleft (C,D\webright )\to \mathrm{Rel}\webleft (A\times C,B\times D\webright ) \]
of $\times $ is given by sending a pair of morphisms $\webleft (R,S\webright )$ of the form
\begin{align*} R & \colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B,\\ S & \colon C\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}D \end{align*}
to the relation
\[ R\times S\colon A\times C\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B\times D \]
of Chapter 7: Constructions With Relations, Definition 7.3.9.1.1.
6.2.3.2 The Monoidal Unit
The monoidal unit of $\mathsf{Rel}$ is the functor
\[ \mathbb {1}^{\mathsf{Rel}}\colon \text{pt}\to \mathsf{Rel} \]
picking the set
\[ \mathbb {1}_{\mathsf{Rel}}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{pt} \]
of $\mathsf{Rel}$.
6.2.3.3 The Associator
The associator of $\mathsf{Rel}$ is the natural isomorphism
\[ \alpha ^{\mathsf{Rel}}\colon {\times }\circ {\webleft ({\webleft (\times \webright )}\times {\mathsf{id}}\webright )}\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}{\times }\circ {\webleft ({\mathsf{id}}\times {\webleft (\times \webright )}\webright )}\circ {\mathbf{\alpha }^{\mathsf{Cats}}_{\mathsf{Rel},\mathsf{Rel},\mathsf{Rel}}}\mathrlap {,} \]
as in the diagram
whose component
\[ \alpha ^{\mathsf{Rel}}_{A,B,C}\colon \webleft (A\times B\webright )\times C\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A\times \webleft (B\times C\webright ) \]
at $A,B,C\in \text{Obj}\webleft (\mathsf{Rel}\webright )$ is the relation defined by declaring
\[ \webleft (\webleft (a,b\webright ),c\webright ) \sim _{\alpha ^{\mathsf{Rel}}_{A,B,C}} \webleft (a',\webleft (b',c'\webright )\webright ) \]
iff $a=a'$, $b=b'$, and $c=c'$.
6.2.3.4 The Left Unitor
The left unitor of $\mathsf{Rel}$ is the natural isomorphism
whose component
\[ \lambda ^{\mathsf{Rel}}_{A} \colon \mathbb {1}_{\mathsf{Rel}}\times A \mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A \]
at $A$ is defined by declaring
\[ \webleft (\star ,a\webright ) \sim _{\lambda ^{\mathsf{Rel}}_{A}} b \]
iff $a=b$.
6.2.3.5 The Right Unitor
The right unitor of $\mathsf{Rel}$ is the natural isomorphism
whose component
\[ \rho ^{\mathsf{Rel}}_{A} \colon A\times \mathbb {1}_{\mathsf{Rel}} \mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A \]
at $A$ is defined by declaring
\[ \webleft (a,\star \webright ) \sim _{\rho ^{\mathsf{Rel}}_{A}} b \]
iff $a=b$.
6.2.3.6 The Symmetry
The symmetry of $\mathsf{Rel}$ is the natural isomorphism
whose component
\[ \sigma ^{\mathsf{Rel}}_{A,B} \colon A\times B \to B\times A \]
at $\webleft (A,B\webright )$ is defined by declaring
\[ \webleft (a,b\webright ) \sim _{\sigma ^{\mathsf{Rel}}_{A,B}} \webleft (b',a'\webright ) \]
iff $a=a'$ and $b=b'$.
6.2.3.7 The Internal Hom
The internal Hom of $\mathsf{Rel}$ is the functor
\[ \mathrm{Rel}\colon \mathsf{Rel}^{\mathsf{op}}\times \mathsf{Rel}\to \mathsf{Rel} \]
defined
Let $A,B,C\in \text{Obj}\webleft (\mathsf{Rel}\webright )$.
-
Adjointness. We have adjunctions witnessed by bijections
\begin{align*} \mathrm{Rel}\webleft (A\times B,C\webright ) & \cong \mathrm{Rel}\webleft (A,\mathrm{Rel}\webleft (B,C\webright )\webright ),\\ \mathrm{Rel}\webleft (A\times B,C\webright ) & \cong \mathrm{Rel}\webleft (B,\mathrm{Rel}\webleft (A,C\webright )\webright ), \end{align*}
natural in $A,B,C\in \text{Obj}\webleft (\mathsf{Rel}\webright )$.
Indeed, we have
\begin{align*} \mathrm{Rel}\webleft (A\times B,C\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{Sets}\webleft (A\times B\times C,\{ \mathsf{true},\mathsf{false}\} \webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Rel}\webleft (A,B\times C\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Rel}\webleft (A,\mathrm{Rel}\webleft (B,C\webright )\webright ), \end{align*}
and similarly for the bijection $\mathrm{Rel}\webleft (A\times B,C\webright )\cong \mathrm{Rel}\webleft (B,\mathrm{Rel}\webleft (A,C\webright )\webright )$.
6.2.3.8 The Closed Symmetric Monoidal Category of Relations
The category $\mathsf{Rel}$ admits a closed symmetric monoidal category structure consisting of1
- The Underlying Category. The category $\mathsf{Rel}$ of sets and relations of Definition 6.2.2.1.1.
- The Monoidal Product. The functor
\[ \times \colon \mathrm{Rel}\times \mathrm{Rel}\to \mathrm{Rel} \]
of Definition 6.2.3.1.1.
- The Internal Hom. The internal Hom functor
\[ \mathbf{Rel}\colon \mathrm{Rel}^{\mathsf{op}}\times \mathrm{Rel}\to \mathrm{Rel} \]
of Definition 6.2.3.7.1.
- The Monoidal Unit. The functor
\[ \mathbb {1}^{\mathrm{Rel}} \colon \mathsf{pt}\to \mathrm{Rel} \]
of Definition 6.2.3.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 6.2.3.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 6.2.3.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 6.2.3.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 6.2.3.6.1.
Omitted.