**Puzzle 91**

Let's start with the first part

> 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) \]

Let's start with the first part

> 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) \]