@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?

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?