Matthew's formula for the associator and its inverse look right, and so does Anindya's proof that the associator is an enriched profunctor!

To prove it's an enriched profunctor, Anindya is using condition 2 in this theorem from [Lecture 63](https://forum.azimuthproject.org/discussion/2295/lecture-63-chapter-4-composing-enriched-profunctors/p1)

> **Theorem.** The following are equivalent:

> 1. \\(\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\\) is a \\(\mathcal{V}\\)-enriched profunctor.

> 2. \\(\mathcal{X}(x', x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x',y')\\) for all \\(x,x',y,y'\\).

> 3. \\(\mathcal{X}(x', x) \otimes \Phi(x, y) \leq \Phi(x', y)\\) and \\(\Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x, y')\\) for all \\(x,x',y,y'\\).

To prove it's an enriched profunctor, Anindya is using condition 2 in this theorem from [Lecture 63](https://forum.azimuthproject.org/discussion/2295/lecture-63-chapter-4-composing-enriched-profunctors/p1)

> **Theorem.** The following are equivalent:

> 1. \\(\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\\) is a \\(\mathcal{V}\\)-enriched profunctor.

> 2. \\(\mathcal{X}(x', x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x',y')\\) for all \\(x,x',y,y'\\).

> 3. \\(\mathcal{X}(x', x) \otimes \Phi(x, y) \leq \Phi(x', y)\\) and \\(\Phi(x, y) \otimes \mathcal{Y}(y, y') \leq \Phi(x, y')\\) for all \\(x,x',y,y'\\).