@Tobias – I think I might have an answer to your **Puzzle TF1**... (it's an adaptation of @Jonathan's attempt at #18)

Let's consider the set of words on an alphabet (including the empty word). This is a monoid by string concatenation.

We will define an A-word to be any word beginning with the letter A.

Consider the following rather ungainly preorder. Every word is \\(\leq\\) itself. But we also have the rule that any A-word is \\(\geq\\) any other word (whether it is an A-word or not). So the preorder is mostly discrete, except with all the A-words lumped together and sitting on top, so to speak.

Now we can check that \\(x\leq x' \Rightarrow x\otimes y\leq x'\otimes y\\) – the only non-trivial case is when \\(x'\\) is an A-word, in which case \\(x'\otimes y\\) is an A-word too.

But we do *not* have \\(y\leq y' \Rightarrow x\otimes y\leq x\otimes y'\\) – consider the case when \\(y'\\) is an A-word, but \\(x\\) is not (eg B \\(\leq\\) A but CB \\(\nleq\\) CA).

So your "one-sided" condition is *not* enough to obtain a monoidal preorder in general.

Let's consider the set of words on an alphabet (including the empty word). This is a monoid by string concatenation.

We will define an A-word to be any word beginning with the letter A.

Consider the following rather ungainly preorder. Every word is \\(\leq\\) itself. But we also have the rule that any A-word is \\(\geq\\) any other word (whether it is an A-word or not). So the preorder is mostly discrete, except with all the A-words lumped together and sitting on top, so to speak.

Now we can check that \\(x\leq x' \Rightarrow x\otimes y\leq x'\otimes y\\) – the only non-trivial case is when \\(x'\\) is an A-word, in which case \\(x'\otimes y\\) is an A-word too.

But we do *not* have \\(y\leq y' \Rightarrow x\otimes y\leq x\otimes y'\\) – consider the case when \\(y'\\) is an A-word, but \\(x\\) is not (eg B \\(\leq\\) A but CB \\(\nleq\\) CA).

So your "one-sided" condition is *not* enough to obtain a monoidal preorder in general.