The Clowder Project

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

where

• •

  Action on Objects. For each $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Rel})$, we have

  \[ \mathord {\times }(A,B)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A\times B, \]

  where $A\times B$ is the Cartesian product of sets of Chapter 4: Constructions With Sets, Definition 4.1.3.1.1.

• •

  Action on Morphisms. For each $(A,C),(B,D)\in \operatorname {\mathrm{Obj}}(\mathsf{Rel}\times \mathsf{Rel})$, the action on morphisms

  \[ \times _{(A,C),(B,D)}\colon \mathrm{Rel}(A,B)\times \mathrm{Rel}(C,D)\to \mathrm{Rel}(A\times C,B\times D) \]

  of $\times $ is given by sending a pair of morphisms $(R,S)$ 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 9: Constructions With Relations, Definition 9.2.6.1.1.