@Marius, Sophie: that's very interesting!

It may be worth pointing out that your result
> **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.

generalizes [Matthew's proposed solution to Puzzle 71](https://forum.azimuthproject.org/discussion/comment/18065/#Comment_18065×), which turns the complex numbers into a commutative monoidal preorder. Do you see how?