John wrote:

>> As a note, Anindya remarks in comment #22 of Lecture 62, there may be issues with that lattice identity I have tried to use...
>
> I don't see any problem with that. Suppose we have a poset \\(\mathcal{V}\\) with all joins, and a doubly indexed family of elements in \\(\mathcal{V}\\), say \\( \lbrace v_{a b} \rbrace_{a \in A, b \in B} \\) where \\(A\\) and \\(B\\) are arbitrary sets. Then
>
> \[ \bigvee_{a \in A} \bigvee_{b \in B} v_{ab} = \bigvee_{a \in A, b \in B} v_{ab} = \bigvee_{b \in B} \bigvee_{a \in A} v_{ab} \]
>
> It takes a bit of work to show this, but it seems so obvious I don't have the energy right now.

I think Anindya is wondering about how this generalizes to a categorical setting, using an *end* like Bartosz Milewski uses in his treatment of [profunctor optics](https://bartoszmilewski.com/2017/07/07/profunctor-optics-the-categorical-view/) on his blog.

I'll try a proof, however. In any semilattice with arbitrary joins, we have the following chain of equivalences:

\[
\begin{align}
\bigvee_{a \in A} \bigvee_{b \in B} \phi(a,b) \leq X & \iff \text{for all } a \text{ in } A \text{: } \bigvee_{b \in B} \phi(a,b) \leq X \\\\
& \iff \text{for all } a \text{ in } A \text{, for all } b \text{ in } B \text{: } \phi(a,b) \leq X \\\\
& \iff \text{for all } b \text{ in } B \text{, for all } a \text{ in } A \text{: } \phi(a,b) \leq X \\\\
& \iff \text{for all } b \text{ in } B \text{: } \bigvee_{a \in A} \phi(a,b) \leq X \\\\
& \iff \bigvee_{b \in B} \bigvee_{a \in A} \phi(a,b) \leq X \\\\
\end{align}
\]

We know that \\(\bigvee_{a \in A} \bigvee_{b \in B} \phi(a,b) \leq \bigvee_{a \in A} \bigvee_{b \in B} \phi(a,b)\\), hence \\(\bigvee_{b \in B} \bigvee_{a \in A} \phi(a,b) \leq \bigvee_{a \in A} \bigvee_{b \in B} \phi(a,b)\\). Symmetrically we have \\(\bigvee_{a \in A} \bigvee_{b \in B} \phi(a,b) \leq \bigvee_{b \in B} \bigvee_{a \in A} \phi(a,b)\\), hence \\(\bigvee_{a \in A} \bigvee_{b \in B} \phi(a,b) = \bigvee_{b \in B} \bigvee_{a \in A} \phi(a,b) \\).

I know I'm like a dog with a bone with this stuff, but argument rests on a first order logic tautology:

\[
\forall x. \phi(x) \to (\forall y. \psi(y) \to \chi(x,y)) \iff \forall y. \psi(y) \to (\forall x. \phi(x) \to \chi(x,y))
\]