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))$