**Puzzle 91**

> Show how to make the product of symmetric monoidal posets into a symmetric monoidal poset.

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)$

Proving that this is a symmetric monoidal poset follows pretty immediately from breaking down each property into a property about \$$(X, \leq_X, I_X, \otimes_X)\$$ and a property about \$$(Y, \leq_Y, I_Y, \otimes_Y)\$$ and then applying the fact that they are both symmetric monoidal posets.

Here is an example:

We want to show that if \$$(x_1, y_1) \leq_{X \times Y} (x_1', y_1') \$$ and \$$(x_2, y_2) \leq_{X \times Y} (x_2', y_2') \$$, then \$(x_1, y_1)\otimes_{X \times Y} (x_2, y_2) \leq_{X \times Y} (x_1', y_1')\otimes_{X \times Y} (x_2', y_2') . \$

By the definition of \$$\leq_{X \times Y}\$$, the hypotheses imply that

$x_1 \leq_X x_1' ,\quad x_2 \leq_X x_2' ,\quad y_1 \leq_Y y_1' , \quad \textrm{ and } y_2 \leq_Y y_2' .$

Since \$$(X, \leq_X, I_X, \otimes_X)\$$ and \$$(Y, \leq_Y, I_Y, \otimes_Y)\$$ are monoidal posets we have that

$x_1 \otimes_X x_2 \leq_X x_1' \otimes_X x_2' \textrm{ and } y_1 \otimes_Y y_2 \leq_Y y_1' \otimes_Y y_2'$

And so by the definition of \$$\leq_{X \times Y}\$$,

$( x_1 \otimes_X x_2, y_1 \otimes_Y y_2 ) \leq_{X \times Y} (x_1' \otimes_X x_2', y_1' \otimes_Y y_2' ).$

Of course applying the definition of \$$\otimes_{X \times Y}\$$ gives us our desired result:

$(x_1, y_1)\otimes_{X \times Y} (x_2, y_2) \leq_{X \times Y} (x_1', y_1')\otimes_{X \times Y} (x_2', y_2') .$

Now onto the next part

> Thus, \$$\mathcal{V} \$$ becomes a symmetric monoidal poset. What is a \$$\mathcal{V} \$$-category like, and what are they good for in everyday life?

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. For example, my commute to and from work is very bad on Monday - Thursday, it's a little better on Friday because some people work from home, and on Saturday and Sunday it's very good. So as a objects of a \$$\mathcal{V} \$$-category, I might represent this as

$\mathcal{X}( \textrm{home}, \textrm{work}) = (30, 30, 30, 30, 25, 15, 15)$