Thought I'd update/fix my previous attempt at proving the first snake inequality given the conventions we've settled on for cap and cup. I've also restricted it to the case where \$$\mathcal{V} = \textbf{Bool}\$$, although the proof works in the general case too.

The first snake inequality concerns the following row of profunctors:

$X \cong \textbf{1} \times X \nrightarrow (X \times X^\text{op}) \times X \cong X \times (X^\text{op} \times X) \nrightarrow X \times \textbf{1} \cong X$

Given any objects \$$x, y\$$ in \$$X\$$ the value of the composite profunctor at \$$(x, y)\$$ is

$\bigvee\big(\Phi((\bullet, x), (z, z', z'')) \otimes \Psi((z, z', z''), (y, \bullet))\big)$

where we're joining over triples \$$(z, z', z'')\$$ in \$$X \times X^\text{op} \times X\$$ and

$\Phi((\bullet, x), (z, z', z'')) = \cap_X(\bullet, (z, z')) \wedge \text{1}_X(x, z'') = (z' \leq z) \wedge (x \leq z'')$

$\Psi((z, z', z''), (y, \bullet)) = \text{1} _X(z, y) \wedge \cup_X((z', z''), \bullet) = (z \leq y) \wedge (z'' \leq z')$

So our join is

$\bigvee\big((z' \leq z) \wedge (x \leq z'') \wedge (z \leq y) \wedge (z'' \leq z')\big)$

Reorder the terms to get

$\bigvee\big((x \leq z'') \wedge (z'' \leq z') \wedge (z' \leq z) \wedge (z \leq y) \big)$

Now if this join is true, then the "summand" must be true for some triple \$$(z, z', z'')\$$, and that implies \$$(x \leq y)\$$.

Conversely, if \$$(x \leq y)\$$ then the "summand" is true for the triple \$$(x, x, x)\$$, so the join is true.

Hence the join is true iff \$$(x \leq y)\$$, so the composite profunctor equals the identity profunctor. QED.