**First snake equation**.

We can show that the diagrams for the snake equation are equal in terms of feasibility relations by expanding the right hand side (RHS) and showing it equals the identity on \\(X\\).

\[ \left(1_X \times \cup_X \right)\left(\cap_X \times 1_X\right) = 1_X \]

Each of these definitions a function from the product of their inputs and outputs to \\(\mathbf{Bool}\\).

The first part is cap and the identity: \\((\cap_X \times 1_X ) : 1 \times X \nrightarrow X \times X^\mathrm{op} \times X\\)

\[(\cap_X \times 1_X )((\bullet,x),(x',x^\ast,x'')) = (x^\ast \le x') \ \mathrm{and} \ (x \le x'') \]

where \\(\bullet \in 1\\).

Dually, we get \\((1_X \times \cup_X ) : X \times X^\mathrm{op} \times X \nrightarrow X \times 1\\)

\[(1_X \times \cup_X )((x',x^\ast,x''),(x,\bullet)) = (x'' \le x^\ast) \ \mathrm{and} \ (x' \le x) \]

Composing, we get

\[ (1_X \times \cup_X ) (\cap_X \times 1_X )((\bullet,x),(x,\bullet)) = x \le x'' \le x^\ast \le x' \le x \]

where the composite is true only if we can find one \\(x'',x^\ast,x'\\) in \\(X\\) such that \\(x\le x\\), but this is always true since we can set \\(x = x' = x'' = x^\ast\\).

Therefore \\((1_X \times \cup_X ) (\cap_X \times 1_X ) \simeq 1_X\\). Equality holds if \\(X \otimes 1 = X = 1 \otimes X\\) because \\((1_X \times \cup_X ) (\cap_X \times 1_X ) : 1\otimes X \nrightarrow X \otimes 1 \\).

**Second snake equation**

Same as above, but with opposite preorders (i.e., turn the arrows around).

\[ (1_{X^\mathrm{op}} \times \cap_{X^\mathrm{op}})((x,\bullet),(x',x^\ast,x'')) = x'' \le x^\ast \ \mathrm{and} \ x' \le x \]

and

\[ (\cup_{X^\mathrm{op}} \times 1_{X^\mathrm{op}})((x',x^\ast,x''),(\bullet,x)) = x^\ast \le x' \ \mathrm{and} \ x \le x'' \]

Composing gives

\[ (\cup_{X^\mathrm{op}} \times 1_{X^\mathrm{op}})(1_{X^\mathrm{op}} \times \cap_{X^\mathrm{op}})((x,\bullet),(\bullet,x)) = x \le x'' \le x^\ast \le x' \le x \]

for some choice of \\(x'',x^\ast,x'\\) in \\(X\\), but again this is always possible since we can choose \\(x = x' = x'' = x^\ast\\).

This composite behaves the same as the identity on \\(X^\mathrm{op}\\), the dual object of \\(X\\).

**Edits:** Changed the name of the element in 1 from 1 to \\(\bullet\\). Also see Yoav's comment since I only prove that the two profunctors are equal along their diagonal.

We can show that the diagrams for the snake equation are equal in terms of feasibility relations by expanding the right hand side (RHS) and showing it equals the identity on \\(X\\).

\[ \left(1_X \times \cup_X \right)\left(\cap_X \times 1_X\right) = 1_X \]

Each of these definitions a function from the product of their inputs and outputs to \\(\mathbf{Bool}\\).

The first part is cap and the identity: \\((\cap_X \times 1_X ) : 1 \times X \nrightarrow X \times X^\mathrm{op} \times X\\)

\[(\cap_X \times 1_X )((\bullet,x),(x',x^\ast,x'')) = (x^\ast \le x') \ \mathrm{and} \ (x \le x'') \]

where \\(\bullet \in 1\\).

Dually, we get \\((1_X \times \cup_X ) : X \times X^\mathrm{op} \times X \nrightarrow X \times 1\\)

\[(1_X \times \cup_X )((x',x^\ast,x''),(x,\bullet)) = (x'' \le x^\ast) \ \mathrm{and} \ (x' \le x) \]

Composing, we get

\[ (1_X \times \cup_X ) (\cap_X \times 1_X )((\bullet,x),(x,\bullet)) = x \le x'' \le x^\ast \le x' \le x \]

where the composite is true only if we can find one \\(x'',x^\ast,x'\\) in \\(X\\) such that \\(x\le x\\), but this is always true since we can set \\(x = x' = x'' = x^\ast\\).

Therefore \\((1_X \times \cup_X ) (\cap_X \times 1_X ) \simeq 1_X\\). Equality holds if \\(X \otimes 1 = X = 1 \otimes X\\) because \\((1_X \times \cup_X ) (\cap_X \times 1_X ) : 1\otimes X \nrightarrow X \otimes 1 \\).

**Second snake equation**

Same as above, but with opposite preorders (i.e., turn the arrows around).

\[ (1_{X^\mathrm{op}} \times \cap_{X^\mathrm{op}})((x,\bullet),(x',x^\ast,x'')) = x'' \le x^\ast \ \mathrm{and} \ x' \le x \]

and

\[ (\cup_{X^\mathrm{op}} \times 1_{X^\mathrm{op}})((x',x^\ast,x''),(\bullet,x)) = x^\ast \le x' \ \mathrm{and} \ x \le x'' \]

Composing gives

\[ (\cup_{X^\mathrm{op}} \times 1_{X^\mathrm{op}})(1_{X^\mathrm{op}} \times \cap_{X^\mathrm{op}})((x,\bullet),(\bullet,x)) = x \le x'' \le x^\ast \le x' \le x \]

for some choice of \\(x'',x^\ast,x'\\) in \\(X\\), but again this is always possible since we can choose \\(x = x' = x'' = x^\ast\\).

This composite behaves the same as the identity on \\(X^\mathrm{op}\\), the dual object of \\(X\\).

**Edits:** Changed the name of the element in 1 from 1 to \\(\bullet\\). Also see Yoav's comment since I only prove that the two profunctors are equal along their diagonal.