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]( Matthew proved 2 in [comment #37 on that lecture](, and Anindya gave a different proof in [comment #9](

Both these are useful facts, but item 1 is so important that I went back and added a proof sketch to [Lecture 63]( 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](, 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](, _Encyclopedia of Mathematics_.

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

* [Idempotent analysis](, _Encyclopedia of Mathematics_.