Hey Anindya,

> 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".

I came up with *complete* because it is a complete rig and complete upper semilattice, but you are right this is a unital quantale. I am going to go back and fix this.

> 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.

Well... in the case that \\(\mathrm{Obj}(\mathcal{X})\\) is a set and we are working in a rig where \\(\sum = \bigvee\\) such as a quantale, the little identity holds. It has to do with the fact that \\(\bigvee_{x \in X}\Xi(x) \otimes -\\) is an upper semi-lattice homomorphism. In the case of feasibility relations, it reflects the FOL identity \\(\exists x. \exists y. \phi(x,y) \iff \exists y. \exists x. \phi(x,y)\\). But we can think of situations where \\(\mathrm{Obj}(\mathcal{X})\\) is a list or even a transfinite sequence, such as in Bayesian updating with some evidence or some other setting. I don't know if we can still meaningfully talk about profunctor composition in rigs where \\(\sum\_{x \in X} \sum\_{y \in Y} \Xi(x,y) \neq \sum\_{y \in Y} \sum_{x \in X} \Xi(x,y)\\), but maybe we can...

Good thing we have experts like Simon and John around, because I am a 100% amateur here and I know I can't dive into the details to your satisfaction :-(