Hey, Dan, that stuff looks really good! I'm about to step out so for now just a quick remark. The identity profunctor

\[ 1_{\mathcal{X}} \colon \mathcal{X} \nrightarrow \mathcal{X} \]

is defined by

\[ 1_{\mathcal{X}}(x,y) = \mathcal{X}(x,y) .\]

In other words, it's just the hom-functor in disguise. So, this equation:

\[
\bigvee_{y} \mathcal{X}(x, y) \otimes \mathcal{X}(y, z) = \mathcal{X}(x, z).
\]

says that the identity profunctor composed with itself is the identity profunctor. That's gotta be true!

And indeed, in [Lecture 64](https://forum.azimuthproject.org/discussion/2298/lecture-64-chapter-5-the-category-of-enriched-profunctors/p1) there's a proof that the identity profunctor works as advertised: composing it with any other profunctor doesn't do anything. So, that proof gives this equation:

\[
\bigvee_{y} \mathcal{X}(x, y) \otimes \mathcal{X}(y, z) = \mathcal{X}(x, z).
\]

as a special case!

But it looks like you proved this equation directly. And it looks like you used the same argument.