The Clowder Project

The monoidal product of $\mathsf{Rel}$ is the functor

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.