And regarding this one:

> **Puzzle 77.** Now suppose that \\( (Y, \le_Y, \otimes_Y, 1_Y) \\) is a monoidal preorder, and \\( (X,\otimes_X,1_X ) \\) is a monoid. Define \\(\le_X\\) as above. Under what conditions on \\(f\\) can we conclude that \\( (X,\le_X\otimes_X,1_X) \\) is a monoidal preorder?

Sophie wrote:

> **Claim** If \\( f(x) \otimes_Y f(x') = f( x \otimes_X x')\\) then the relation \\(\leq_X\\) induced by \\(f\\) makes \\( (X, \otimes_X, 1_X, \leq_X) \\) a monoidal preorder.

Yes, that's right! So this is a sufficient condition, and this is the answer I had in mind.

You suggest that a weaker condition may be enough:

\[ f( x \otimes_X x') \le f(x) \otimes_Y f(x') \qquad \star \]

for all \\(x,x' \in X\\).

Let's see. To prove \\(\leq_X\\) is a monoidal preorder, we need to prove

\[ x_1 \le_X x_1' \textrm{ and } x_2 \le_X x_2' \textrm{ imply } x_1 \otimes_X x_2 \le_X x_1' \otimes_X x_2' \]

for all \\(x_1,x_1',x_2,x_2' \in X\\). In other words, we need

\[ f(x_1) \le_Y f(x_1') \textrm{ and } f(x_2) \le_Y f(x_2') \textrm{ imply } f(x_1 \otimes_X x_2) \le_Y f(x_1' \otimes_X x_2') . \]

On the other hand, since \\( (Y, \le_Y, \otimes_Y, 1_Y) \\) is a monoidal preorder, we know that

\[ f(x_1) \le_Y f(x_1') \textrm{ and } f(x_2) \le_Y f(x_2') \textrm{ imply } f(x_1)\otimes_Y f(x_2) \le_Y f(x_1') \otimes_Y f(x_2') . \]

If we assume condition \\(\star\\), we also know

\[ f(x_1 \otimes_X x_2) \le_Y f(x_1)\otimes_Y f(x_2) . \]

Combining this with what we know, we get

\[ f(x_1) \le_Y f(x_1') \textrm{ and } f(x_2) \le_Y f(x_2') \textrm{ imply } f(x_1 \otimes_X x_2) \le_Y f(x_1') \otimes_Y f(x_2') . \]

But this does not yet get us what we need! Remember, we need

\[ f(x_1) \le_Y f(x_1') \textrm{ and } f(x_2) \le_Y f(x_2') \textrm{ imply } f(x_1 \otimes_X x_2) \le_Y f(x_1' \otimes_X x_2') . \]

The obvious way to get this is to also assume

\[ f(x) \otimes_Y f(x') \le f(x \otimes_X x') \qquad \star\star \]

for all \\(x,x' \in X\\). But \\(\star\\) together with \\(\star\star\\) is just your earlier condition

\[ f(x) \otimes_Y f(x') = f(x \otimes_X x') \]

I don't see how either \\(\star\\) or \\(\star\star\\) is enough for this problem. I don't think either one by itself will do the job.