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.