**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) \]
Version 2.1.8p2
