@John wrote:

> Here's a thought: you could try to define the associator and its inverse as companions of enriched functors that are clearly inverses of each other, and then prove \\(\widehat{FG} = \widehat{F}\circ\widehat{G}\\)... This might require less calculation than a direct approach: for example, you wouldn't have to prove the associator and its inverse are profunctors. It would also develop some general tools that could be reused.

OK let's try this. We had a look at composing companions back in [Lecture 66](https://forum.azimuthproject.org/discussion/comment/20385/#Comment_20385) so I'm adapting some stuff from there.

\[\]

First, let's prove that \\(\widehat{F} \circ \widehat{G} = \widehat{FG}\\), where \\(F : \mathcal{Y} \to \mathcal{Z}, G : \mathcal{X} \to \mathcal{Y}\\).

\[(\widehat{F} \circ \widehat{G})(x, z) = \bigvee\big(\widehat{G}(x, y) \otimes \widehat{F}(y, z)\big) = \bigvee\big(\mathcal{Y}(Gx, y) \otimes \mathcal{Z}(Fy, z)\big)\]

It turns out that this join \\(= \mathcal{Z}(FGx, z) = \widehat{FG}(x, z)\\).

To prove this, first set \\(y = Gx\\) to see that our join \\(\geq \mathcal{Y}(Gx, Gx) \otimes \mathcal{Z}(FGx, z) \geq I \otimes \mathcal{Z}(FGx, z) = \mathcal{Z}(FGx, z)\\)

But given any \\(y\\) we have \\(\mathcal{Z}(FGx, z) \geq \mathcal{Z}(FGx, Fy) \otimes \mathcal{Z}(Fy, z) \geq \mathcal{Y}(Gx, y) \otimes \mathcal{Z}(Fy, z)\\)

So we also have \\(\mathcal{Z}(FGx, z) \geq\\) our join. QED

\[\]

Second, note that the companion of the identity \\(\mathcal{V}\\)-functor \\(\mathcal{X}\to\mathcal{X}\\) is the identity profunctor \\(\mathcal{X}\nrightarrow\mathcal{X}\\).

It follows that if \\(F\\) and \\(G\\) are inverses, then the profunctors \\(\widehat{F}\\) and \\(\widehat{G}\\) are inverses, ie isomorphisms in the category \\(\textbf{Prof}\\).

\[\]

Third, let's define \\(A : (\mathcal{X}\otimes\mathcal{Y})\otimes\mathcal{Z} \to \mathcal{X}\otimes(\mathcal{Y}\otimes\mathcal{Z})\\) and \\(B : \mathcal{X}\otimes(\mathcal{Y}\otimes\mathcal{Z}) \to (\mathcal{X}\otimes\mathcal{Y})\otimes\mathcal{Z}\\) by

\[A\langle\langle x, y\rangle, z\rangle = \langle x, \langle y, z\rangle\rangle \qquad B\langle x, \langle y, z\rangle\rangle = \langle\langle x, y\rangle, z\rangle\]

It's easy to check that \\(A\\) and \\(B\\) are indeed \\(\mathcal{V}\\)-functors, and they are obviously mutually inverse.

\[\]

Finally, what is \\(\widehat{A}\\)? By the definition of a companion we have

\[\widehat{A}(\langle\langle x, y\rangle, z\rangle, \langle x', \langle y', z'\rangle\rangle) = (\mathcal{X}\otimes(\mathcal{Y}\otimes\mathcal{Z}))(A\langle\langle x, y\rangle, z\rangle, \langle x', \langle y', z'\rangle\rangle)\]

\[= (\mathcal{X}\otimes(\mathcal{Y}\otimes\mathcal{Z}))(\langle x, \langle y, z\rangle\rangle, \langle x', \langle y', z'\rangle\rangle) = \mathcal{X}(x, x') \otimes \mathcal{Y}(y, y') \otimes \mathcal{Z}(z, z')\]

which is our associator one way, and similarly \\(\widehat{B}\\) is the associator the other way. Combining this with the previous results, we have proved that the associators are profunctors and that they are inverse to each other.

> Here's a thought: you could try to define the associator and its inverse as companions of enriched functors that are clearly inverses of each other, and then prove \\(\widehat{FG} = \widehat{F}\circ\widehat{G}\\)... This might require less calculation than a direct approach: for example, you wouldn't have to prove the associator and its inverse are profunctors. It would also develop some general tools that could be reused.

OK let's try this. We had a look at composing companions back in [Lecture 66](https://forum.azimuthproject.org/discussion/comment/20385/#Comment_20385) so I'm adapting some stuff from there.

\[\]

First, let's prove that \\(\widehat{F} \circ \widehat{G} = \widehat{FG}\\), where \\(F : \mathcal{Y} \to \mathcal{Z}, G : \mathcal{X} \to \mathcal{Y}\\).

\[(\widehat{F} \circ \widehat{G})(x, z) = \bigvee\big(\widehat{G}(x, y) \otimes \widehat{F}(y, z)\big) = \bigvee\big(\mathcal{Y}(Gx, y) \otimes \mathcal{Z}(Fy, z)\big)\]

It turns out that this join \\(= \mathcal{Z}(FGx, z) = \widehat{FG}(x, z)\\).

To prove this, first set \\(y = Gx\\) to see that our join \\(\geq \mathcal{Y}(Gx, Gx) \otimes \mathcal{Z}(FGx, z) \geq I \otimes \mathcal{Z}(FGx, z) = \mathcal{Z}(FGx, z)\\)

But given any \\(y\\) we have \\(\mathcal{Z}(FGx, z) \geq \mathcal{Z}(FGx, Fy) \otimes \mathcal{Z}(Fy, z) \geq \mathcal{Y}(Gx, y) \otimes \mathcal{Z}(Fy, z)\\)

So we also have \\(\mathcal{Z}(FGx, z) \geq\\) our join. QED

\[\]

Second, note that the companion of the identity \\(\mathcal{V}\\)-functor \\(\mathcal{X}\to\mathcal{X}\\) is the identity profunctor \\(\mathcal{X}\nrightarrow\mathcal{X}\\).

It follows that if \\(F\\) and \\(G\\) are inverses, then the profunctors \\(\widehat{F}\\) and \\(\widehat{G}\\) are inverses, ie isomorphisms in the category \\(\textbf{Prof}\\).

\[\]

Third, let's define \\(A : (\mathcal{X}\otimes\mathcal{Y})\otimes\mathcal{Z} \to \mathcal{X}\otimes(\mathcal{Y}\otimes\mathcal{Z})\\) and \\(B : \mathcal{X}\otimes(\mathcal{Y}\otimes\mathcal{Z}) \to (\mathcal{X}\otimes\mathcal{Y})\otimes\mathcal{Z}\\) by

\[A\langle\langle x, y\rangle, z\rangle = \langle x, \langle y, z\rangle\rangle \qquad B\langle x, \langle y, z\rangle\rangle = \langle\langle x, y\rangle, z\rangle\]

It's easy to check that \\(A\\) and \\(B\\) are indeed \\(\mathcal{V}\\)-functors, and they are obviously mutually inverse.

\[\]

Finally, what is \\(\widehat{A}\\)? By the definition of a companion we have

\[\widehat{A}(\langle\langle x, y\rangle, z\rangle, \langle x', \langle y', z'\rangle\rangle) = (\mathcal{X}\otimes(\mathcal{Y}\otimes\mathcal{Z}))(A\langle\langle x, y\rangle, z\rangle, \langle x', \langle y', z'\rangle\rangle)\]

\[= (\mathcal{X}\otimes(\mathcal{Y}\otimes\mathcal{Z}))(\langle x, \langle y, z\rangle\rangle, \langle x', \langle y', z'\rangle\rangle) = \mathcal{X}(x, x') \otimes \mathcal{Y}(y, y') \otimes \mathcal{Z}(z, z')\]

which is our associator one way, and similarly \\(\widehat{B}\\) is the associator the other way. Combining this with the previous results, we have proved that the associators are profunctors and that they are inverse to each other.