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...