The Clowder Project

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

where

• Action on Objects. For each $A,B\in \text{Obj}\left(\mathsf{Rel}\right)$, we have
  $$\times (A,B)\stackrel{\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 $(A,C),(B,D)\in \text{Obj}(\mathsf{Rel}\times \mathsf{Rel})$, the action on morphisms
  $${\times }_{(A,C),(B,D)}:\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{array}{rl}R& :A\to |B,\\ S& :C\to |D\end{array}$$

  to the relation

  $$R\times S:A\times C\to |B\times D$$

  of Chapter 7: Constructions With Relations, Definition 7.3.9.1.1.