Anindya wrote:

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

Yes. 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} \widehat{G} . \]

Do you see where I'm wanting to go with this?

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.

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

Yes. 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} \widehat{G} . \]

Do you see where I'm wanting to go with this?

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.