With regard to the monoidal product distributing over the joins, note here how the two languages do not mesh together well. In the lattice theoretic world, you impose that the monoidal product distributes over joins, whereas in the category theoretic world you impose that the monoidal product preserves the order. Are these equivalent? Is there a monoidal preorder in which the monoidal product does not distribute over joins?