Thanks Sophie for re-posting my comment in the right place and for your nice proof that \$$f\$$ must be injective! Regarding:

> I was interested that this is the opposite condition from what Marius proposed.

I just took the definition for a monoidal monotone from 7 sketches p.46 without thinking it through all that much. Given your example in comment 6, I see that in our interpretation of grocery shopping and resource theories your condition seems to make more sense. Batching processes usually results in lower costs and/or more products. My condition could also be the case in grocery shopping, however.

**Example** Consider that you have a bunch of coupons for the grocery store giving you a flat 0.50\$ discount. However, you may only use one coupon per visit to the store. This means that "the cost of buying two sets of groceries separately is *less* than the cost of buying them together".

I think we need to also reverse the inequality in the second condition if we stick to your condition. It might be instructive to consider monoidal monotone maps between monoidal preorders with different units to think about this. For example \$$f: (\mathbb{N},\le, +, 0) \hookrightarrow (\mathbb{N},\le, *, 1) \$$ or \$$g: (\mathbb{N},\le, *, 1) \hookrightarrow (\mathbb{N},\le, +, 0) \$$, where \$$f \$$ and \$$g \$$ are the inclusions.

For \$$f\$$ it is the case that \$$f(x) \otimes_Y f(y) \ge_Y f(x \otimes_X y) \$$ and \$$1_Y \ge_Y f(1_X)\$$. For \$$g\$$ it is the case that \$$g(x) \otimes_Y g(y) \le_Y g(x \otimes_X y) \$$ and \$$1_Y \le_Y g(1_X)\$$.

So based on this one example it seems that either condition works as long as one is consistent. This means that for \$$1_Y = f(1_X)\$$ we could use either inequality.

*Edit:* Just realized we probably only need one version of the conditions since we can formally take the function to the opposite preorder to get the other.