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.
