The proofs are a bit more terse than I'd like; unfortunately there's a limit on the number of characters per post and I'm up against it, so I can't put in as many steps as I should!

The biggest holes are proving:

1. \$$\otimes\$$ distributes over \$$\bigvee\$$ in a commutative quantale.

2. \$$\bigvee_x \bigvee_y v_{xy} = \bigvee_y \bigvee_x v_{xy} \$$ whenever \$$v_{xy}\$$ is a doubly indexed collection of elements in a poset and the joins in question exist.

I proved most of item 1 in [comment #2 on Lecture 63](https://forum.azimuthproject.org/discussion/comment/20227/#Comment_20227). Matthew proved 2 in [comment #37 on that lecture](https://forum.azimuthproject.org/discussion/comment/20237/#Comment_20237), and Anindya gave a different proof in [comment #9](https://forum.azimuthproject.org/discussion/comment/20243/#Comment_20243).

Both these are useful facts, but item 1 is so important that I went back and added a proof sketch to [Lecture 63](https://forum.azimuthproject.org/discussion/2295/lecture-63-chapter-4-composing-enriched-profunctors/p1). More precisely, I sketched a proof of this stronger fact:

**Theorem.** If \$$\mathcal{V}\$$ is a monoidal poset with all joins, \$$\mathcal{V}\$$ is a quantale if and only if

$a \otimes \left( \bigvee\_{b\in B} b\right) = \bigvee\_{b \in B} (a \otimes b)$

for every element \$$a\$$ and every subset \$$B\$$ of \$$\mathcal{V}\$$.

This theorem implies that a commutative quantale is a lot like a commutative ring: it has a commutative multiplication \$$\otimes\$$ which distributes over \$$\bigvee\$$ on _both sides_. (Above we only get distributivity on the left, but if \$$\otimes\$$ is commutative we get it on both sides!)

Indeed, any commutative quantale is an example of a commutative [rig](https://en.wikipedia.org/wiki/Semiring), or 'ring without negatives', if we define multiplication by \$$xy = x \otimes y\$$ and addition by \$$x + y = x \vee y\$$. But it's much better than just a commutative rig, because we can add _infinitely many_ elements using \$$\bigvee\$$. In other words, we get a commutative rig where _all sums converge_. This is why we can compose enriched profunctors using 'matrix multiplication' even when our matrices are infinite in size.

Addition defined by \$$x + y = x \vee y\$$ also has the curious but very nice property that \$$x + x = x \$$. A rig obeying this property is called an **idempotent rig** or **idempotent semiring**:

* [Idempotent semi-ring](https://www.encyclopediaofmath.org/index.php/Idempotent_semi-ring), _Encyclopedia of Mathematics_.

These are important in 'idempotent analysis', a subject with lots of interesting applications:

* [Idempotent analysis](https://www.encyclopediaofmath.org/index.php/Idempotent_analysis), _Encyclopedia of Mathematics_.