Scott, your snake equation proof looks good, except that you only show that the two profunctors are equal along the diagonal. That is, you only show that for all \\(x\\),

\[ (1_X \times \cup_X ) (\cap_X \times 1_X )((1,x),(x,1)) = 1_X(x,x) \]

You need to show that for all \\(x,\tilde{x}\\),

\[ (1_X \times \cup_X ) (\cap_X \times 1_X )((1,x),(\tilde{x},1)) = 1_X(x,\tilde{x}). \]

Replacing \\(x\\) by \\(\tilde{x}\\) in the appropriate places in your proof, you get that

\\((1_X \times \cup_X ) (\cap_X \times 1_X )((1,x),(\tilde{x},1))\\)

if and only if there exist \\(x'', x^*, x'\\) such that \\(x\le x'' \le x^* \le x' \le \tilde{x}\\),

and of course this hold if and only if \\(x\le\tilde{x}\\) or in other words \\(1_X(x,\tilde{x})\\).

On a stylistic note, I think 0 is better than 1 as the name for the only element in \\(\mathbf{1}\\), as John used in the last lecture. I've seen others here use a bullet or star symbol, which I think are also better than 1.

\[ (1_X \times \cup_X ) (\cap_X \times 1_X )((1,x),(x,1)) = 1_X(x,x) \]

You need to show that for all \\(x,\tilde{x}\\),

\[ (1_X \times \cup_X ) (\cap_X \times 1_X )((1,x),(\tilde{x},1)) = 1_X(x,\tilde{x}). \]

Replacing \\(x\\) by \\(\tilde{x}\\) in the appropriate places in your proof, you get that

\\((1_X \times \cup_X ) (\cap_X \times 1_X )((1,x),(\tilde{x},1))\\)

if and only if there exist \\(x'', x^*, x'\\) such that \\(x\le x'' \le x^* \le x' \le \tilde{x}\\),

and of course this hold if and only if \\(x\le\tilde{x}\\) or in other words \\(1_X(x,\tilde{x})\\).

On a stylistic note, I think 0 is better than 1 as the name for the only element in \\(\mathbf{1}\\), as John used in the last lecture. I've seen others here use a bullet or star symbol, which I think are also better than 1.