Pedantic addendum to @Matthew's solution to **Puzzle 224** – we need to prove the associator really is a profunctor.

Suppose \$$\langle\langle a, b\rangle, c\rangle \leq \langle\langle x, y\rangle, z\rangle\$$ and \$$\langle x', \langle y', z'\rangle\rangle \leq \langle\langle a', b'\rangle, c'\rangle\$$.

This is equivalent to assuming that \$$a \leq x, b \leq y, c \leq z\$$ and \$$x' \leq a', y' \leq b', z' \leq c'\$$.

Then we have:

\$$((\mathcal{X}\otimes \mathcal{Y})\otimes\mathcal{Z})(\langle\langle a, b\rangle, c\rangle, \langle\langle x, y\rangle, z\rangle) \otimes \alpha\_{\mathcal{X}, \mathcal{Y},\mathcal{Z}}(\langle\langle x, y\rangle, z\rangle, \langle x', \langle y', z'\rangle\rangle) \otimes (\mathcal{X}\otimes (\mathcal{Y}\otimes\mathcal{Z}))(\langle x', \langle y', z'\rangle\rangle, \langle a', \langle b', c'\rangle\rangle)\$$

\$$= \big(\mathcal{X}(a, x) \otimes \mathcal{Y}(b, y) \otimes \mathcal{Z}(c, z)\big) \otimes \big(\mathcal{X}(x, x') \otimes \mathcal{Y}(y, y') \otimes \mathcal{Z}(z, z')\big) \otimes \big(\mathcal{X}(x', a') \otimes \mathcal{Y}(y', b') \otimes \mathcal{Z}(z', c')\big)\$$

\$$= \big(\mathcal{X}(a, x) \otimes \mathcal{X}(x, x') \otimes \mathcal{X}(x', a')\big) \otimes \big(\mathcal{Y}(b, y) \otimes \mathcal{Y}(y, y') \otimes \mathcal{Y}(y', b')\big) \otimes \big(\mathcal{Z}(c, z) \otimes \mathcal{Z}(z, z') \otimes \mathcal{Z}(z', c')\big)\$$

\$$\leq \mathcal{X}(a, a') \otimes \mathcal{Y}(b, b') \otimes \mathcal{Z}(c, c')\$$

\$$= \alpha\_{\mathcal{X}, \mathcal{Y},\mathcal{Z}}(\langle\langle a, b\rangle, c\rangle, \langle a', \langle b', c'\rangle\rangle)\$$

So \$$\alpha\_{\mathcal{X}, \mathcal{Y},\mathcal{Z}}\$$ is a profunctor after all. QED

The proof for the inverse is similar. Though it strikes me that we also need to prove that it _is_ an inverse...