Very nice answer to Puzzle 217 in [comment #10](https://forum.azimuthproject.org/discussion/comment/20436/#Comment_20436), Scott!

>Therefore \\((1_X \times \cup_X ) (\cap_X \times 1_X ) \simeq 1_X\\). Equality holds if \\(X \otimes 1 = X = 1 \otimes X\\) because \\((1_X \times \cup_X ) (\cap_X \times 1_X ) : 1\otimes X \nrightarrow X \otimes 1 \\).

Hmm, this is an interesting nuance.

You're right, the claimed equation

\[ (1_X \times \cup_X ) (\cap_X \times 1_X ) = 1_X \]

is not really right, because the right-hand side is a profunctor from \\(X\\) to \\(X\\), while the right is really a profunctor from \\(\mathbf{1} \times X\\) to \\(X \times \mathbf{1}\\).

Luckily, there are god-given isomorphisms called the **left unitor**

\[ \lambda_X \colon \mathbf{1} \times X \nrightarrow X \]

and **right unitor**

\[ \rho_X \colon X \otimes \mathbf{1} \nrightarrow X .\]

(These actually begin life as monotone functions with monotone inverses, but we can convert them into enriched profunctors by taking companions.)

So, a more precise way to state the claimed equation is

\[ \rho_X^{-1} (1_X \times \cup_X ) (\cap_X \times 1_X ) \lambda_X = 1_X .\]

More precise, but not completely precise: there's an even subtler subtlety! The morphism \\(\cap_X \times 1_X\\) has target \\( (X \times X) \times X\\), while the morphism \\(1_X \times \cup_X \\) has source \\( X \times (X \times X)\\). So, you can only compose them if you stick the obvious isomorphism from \\( (X \times X) \times X\\) to \\( X \times (X \times X)\\) between them! This an example of an **associator**

\[ \alpha_{X,Y,Z} \colon (X \times Y) \times Z \nrightarrow X \times (Y \times Z) .\]

All this may be seen as overly fussy by some people. But anyway, the left unitor, right unitor and associator are three main features of a [monoidal category](https://en.wikipedia.org/wiki/Monoidal_category#Formal_definition), and any category of \\(\mathcal{V}\\)-enriched profunctors is a monoidal category!

Soon I will talk about these... and you can read about them in Section 4.4.3 of the book, though you won't see the precise definition.

I hadn't remembered that we already need to think a bit about the unitors and associators to be completely precise about the snake equations. Many less careful people are willing to pretend these are identity morphisms and thus ignorable. This is actually justified by 'Mac Lane's coherence theorem'.

>Therefore \\((1_X \times \cup_X ) (\cap_X \times 1_X ) \simeq 1_X\\). Equality holds if \\(X \otimes 1 = X = 1 \otimes X\\) because \\((1_X \times \cup_X ) (\cap_X \times 1_X ) : 1\otimes X \nrightarrow X \otimes 1 \\).

Hmm, this is an interesting nuance.

You're right, the claimed equation

\[ (1_X \times \cup_X ) (\cap_X \times 1_X ) = 1_X \]

is not really right, because the right-hand side is a profunctor from \\(X\\) to \\(X\\), while the right is really a profunctor from \\(\mathbf{1} \times X\\) to \\(X \times \mathbf{1}\\).

Luckily, there are god-given isomorphisms called the **left unitor**

\[ \lambda_X \colon \mathbf{1} \times X \nrightarrow X \]

and **right unitor**

\[ \rho_X \colon X \otimes \mathbf{1} \nrightarrow X .\]

(These actually begin life as monotone functions with monotone inverses, but we can convert them into enriched profunctors by taking companions.)

So, a more precise way to state the claimed equation is

\[ \rho_X^{-1} (1_X \times \cup_X ) (\cap_X \times 1_X ) \lambda_X = 1_X .\]

More precise, but not completely precise: there's an even subtler subtlety! The morphism \\(\cap_X \times 1_X\\) has target \\( (X \times X) \times X\\), while the morphism \\(1_X \times \cup_X \\) has source \\( X \times (X \times X)\\). So, you can only compose them if you stick the obvious isomorphism from \\( (X \times X) \times X\\) to \\( X \times (X \times X)\\) between them! This an example of an **associator**

\[ \alpha_{X,Y,Z} \colon (X \times Y) \times Z \nrightarrow X \times (Y \times Z) .\]

All this may be seen as overly fussy by some people. But anyway, the left unitor, right unitor and associator are three main features of a [monoidal category](https://en.wikipedia.org/wiki/Monoidal_category#Formal_definition), and any category of \\(\mathcal{V}\\)-enriched profunctors is a monoidal category!

Soon I will talk about these... and you can read about them in Section 4.4.3 of the book, though you won't see the precise definition.

I hadn't remembered that we already need to think a bit about the unitors and associators to be completely precise about the snake equations. Many less careful people are willing to pretend these are identity morphisms and thus ignorable. This is actually justified by 'Mac Lane's coherence theorem'.