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.