Here's another loose end that I thought might be worth tying up – why are we insisting on *symmetric* monoidal preorders? The reason for this is in section 2.4.3 of Seven Sketches, and in particular exercise 2.52 – we need symmetry in order to define the *product* of two \$$\mathcal{V}\$$-enriched categories:

Suppose \$$\mathcal{X}\$$ and \$$\mathcal{Y}\$$ are \$$\mathcal{V}\$$-enriched categories.

Define \$$\mathcal{X} \times \mathcal{Y}\$$ by

\$\textrm{Ob}(\mathcal{X} \times \mathcal{Y}) = Ob(\mathcal{X}) \times Ob(\mathcal{Y})\$

and

\$(\mathcal{X} \times \mathcal{Y})(\langle x_0, y_0\rangle, \langle x_1, y_1\rangle) = \mathcal{X}(x_0, x_1) \otimes \mathcal{Y}(y_0, y_1)\$

Checking the unit law holds:

\$(\mathcal{X} \times \mathcal{Y})(\langle x, y\rangle, \langle x, y\rangle) = \mathcal{X}(x, x) \otimes \mathcal{Y}(y, y) \geq I \otimes I = I\$

Checking the composition law holds:

\$(\mathcal{X} \times \mathcal{Y})(\langle x_0, y_0\rangle, \langle x_1, y_1\rangle) \otimes (\mathcal{X} \times \mathcal{Y})(\langle x_1, y_1\rangle, \langle x_2, y_2\rangle)\$

\$= \mathcal{X}(x_0, x_1) \otimes \mathcal{Y}(y_0, y_1) \otimes \mathcal{X}(x_1, x_2) \otimes \mathcal{Y}(y_1, y_2)\$

(we now use symmetry to swap round the middle two terms)

\$\leq \mathcal{X}(x_0, x_1) \otimes \mathcal{X}(x_1, x_2) \otimes \mathcal{Y}(y_0, y_1) \otimes \mathcal{Y}(y_1, y_2)\$

\$\leq \mathcal{X}(x_0, x_2) \otimes \mathcal{Y}(y_0, y_2)\$

\$= (\mathcal{X} \times \mathcal{Y})(\langle x_0, y_0\rangle, \langle x_2, y_2\rangle)\$

So \$$\mathcal{X} \times \mathcal{Y}\$$ is itself a \$$\mathcal{V}\$$-enriched category.