Sophie wrote:

> Let \$$(X, \leq_X, I_X, \otimes_X)\$$ and \$$(Y, \leq_Y, I_Y, \otimes_Y)\$$. We can define a new symmetric monoidal poset \$$(X\times Y, \leq_{X \times Y}, I_{X \times Y}, \otimes_{X\times Y} ) \$$ where

> $$(x, y) \leq_{X \times Y} (x', y') \textrm{ iff } x \leq_X x' \textrm{ and } y \leq_Y y'$$ $$I_{X \times Y} = (I_X, I_Y)$$ $$(x_1, y_1) \otimes_{X \times Y} (x_2, y_2) = (x_1 \otimes_X x_2, y_1 \otimes_Y y_2)$$

Yes, that's the best way to make \$$X \times Y\$$ into a symmetric monoidal poset! If we ever get around to talking about the category of symmetric monoidal posets, this will be the [product](https://en.wikipedia.org/wiki/Product_(category_theory)) in that category!

(Actually it will be the product even if we _don't_ get around to talking about it.)

> A \$$\mathcal{V} \$$-category assigns to every pair of objects a cost for each day of the week. Projecting to just the costs for one of the days of the week will give you a Lawvere metric space.

> This might be useful when thinking about commutes.

Yes, that's exactly the example I had in mind! Or museum prices: sometimes there's a discount for getting into the museum on certain days of the week.