that's really useful @Matthew – I was wondering where @Simon's comment about \\(\otimes\\) distributing over joins fitted into all this, and that clarifies things nicely. Two quibbles tho:

First, I don't really like the term "complete monoidal poset" – I think "complete" if it means anything means that the *poset* structure is complete, in that it has all joins, ie we should say something like "monoidal complete join-semilattice". Moreover, the distributivity of \\(\otimes\\) over infinite joins strikes me as a very serious new property in its own right, over and above the widget just happening to be both a complete join-semilattice and a monoid, at the same time and in a compatible way. I think it makes sense to come up with a new word for this creature with this extra special property, and "quantale" seems to be what people have settled on. There's an analogy here with the way that when \\(\wedge\\) distributes over infinite joins in a complete lattice, that makes the lattice so unusual we give it a new name, ie "frame" or "locale".

Second – and this is more of an itch on my part – I suspect there's a whole bundle of subtleties wrapped up in what you've called the "upper semilattice identity" – it's easy to prove in this case where the indexing widgets are both sets (\\(\text{Obj}(\mathcal{B})\\) and \\(\text{Obj}(\mathcal{C})\\) respectively). Yes, we can swap round the joins in that case. But are the indexing widgets necessarily sets? If we imagine this as "matrix multiplication" are we not in fact indexing by lists? And what then if we were to index by trees, or by some even more convoluted structure? At what point does "yeah swap round the joins, no problem" cease to work? A rabbit hole beckons.

First, I don't really like the term "complete monoidal poset" – I think "complete" if it means anything means that the *poset* structure is complete, in that it has all joins, ie we should say something like "monoidal complete join-semilattice". Moreover, the distributivity of \\(\otimes\\) over infinite joins strikes me as a very serious new property in its own right, over and above the widget just happening to be both a complete join-semilattice and a monoid, at the same time and in a compatible way. I think it makes sense to come up with a new word for this creature with this extra special property, and "quantale" seems to be what people have settled on. There's an analogy here with the way that when \\(\wedge\\) distributes over infinite joins in a complete lattice, that makes the lattice so unusual we give it a new name, ie "frame" or "locale".

Second – and this is more of an itch on my part – I suspect there's a whole bundle of subtleties wrapped up in what you've called the "upper semilattice identity" – it's easy to prove in this case where the indexing widgets are both sets (\\(\text{Obj}(\mathcal{B})\\) and \\(\text{Obj}(\mathcal{C})\\) respectively). Yes, we can swap round the joins in that case. But are the indexing widgets necessarily sets? If we imagine this as "matrix multiplication" are we not in fact indexing by lists? And what then if we were to index by trees, or by some even more convoluted structure? At what point does "yeah swap round the joins, no problem" cease to work? A rabbit hole beckons.