Michael wrote in [comment #22](https://forum.azimuthproject.org/discussion/comment/20826/#Comment_20826):

> >**Puzzle 284.** Using the cap and cup, any morphism \\(f \colon x \to y \\) in a compact closed category gives rise to a morphism from \\(y^\ast\\) to \\(x^\ast\\). This amounts to 'turning \\(f\\) around' in a certain sense, and we call this morphism \\(f^\ast \colon y^\ast \to x^\ast \\). Write down a formula for \\(f^\ast\\) and also draw it as a string diagram.

> \\(y^\ast \stackrel{\sim}{\to} y^\ast \otimes I \stackrel{1_y \otimes \cap_x}{\to} y^\ast \otimes (x \otimes x^\ast) \stackrel{1_y \otimes (f \otimes 1_x)}{\to} y^\ast \otimes (y \otimes x^\ast) \stackrel{\sim}{\to} (y^\ast \otimes y) \otimes x^\ast \stackrel{\cup_y \otimes 1_x}{\to} I \otimes x^\ast \stackrel{\sim}{\to} x^\ast\\)

> ![function_cap_cup](http://aether.co.kr/images/function_cap_cup.svg)

This looks great! We take

\[ f \colon x \to y ,\]

use a cup to bend its output wire so that the output \\(y\\) becomes the input \\(y^\ast\\), use a cap to bend its input wire so that the input \\(x\\) becomes the output \\(x^\ast\\), and get a morphism we define to be

\[ f^\ast \colon y^\ast \to x^\ast .\]

> So the composite function...

You mean "composite morphism"...

> ...would be \\( f^\ast = (1_y \otimes \cap_x)(1_y \otimes f \otimes 1_x)(\cup_y \otimes 1_x)\\).

This simplified formula is only correct if you're in a _strict_ monoidal category. In your detailed formula

\\(y^\ast \stackrel{\sim}{\to} y^\ast \otimes I \stackrel{1_y \otimes \cap_x}{\to} y^\ast \otimes (x \otimes x^\ast) \stackrel{1_y \otimes (f \otimes 1_x)}{\to} y^\ast \otimes (y \otimes x^\ast) \stackrel{\sim}{\to} (y^\ast \otimes y) \otimes x^\ast \stackrel{\cup_y \otimes 1_x}{\to} I \otimes x^\ast \stackrel{\sim}{\to} x^\ast\\)

you've got some isomorphisms! First you've got the inverse of the right unitor:

\[ \rho_{y^\ast} \colon y^\ast \stackrel{\sim}{\to} y^\ast \otimes I \]

then the inverse of the associator:

\[ \alpha_{y^\ast, y, x^\ast} \colon y^\ast \otimes (y \otimes x^\ast) \stackrel{\sim}{\to} (y^\ast \otimes y) \]

and then the left unitor:

\[ \lambda_{x^\ast} \colon I \otimes x^\ast \stackrel{\sim}{\to} x^\ast \]

In a _strict_ monoidal category these are all identity morphisms. Also, in a strict monoidal category we can write \\(1_y \otimes (f \otimes 1_x)\\) as \\(1_y \otimes f \otimes 1_x \\) since the tensor product is associative. So, if our compact closed category is strict monoidal we can write:

\[ f^\ast = (1_y \otimes \cap_x)(1_y \otimes f \otimes 1_x)(\cup_y \otimes 1_x) .\]

In general, the formula is more complicated. This is one reason string diagrams are convenient: they allow us to hide the associators and unitors. Of course, it takes work to justify the use of string diagrams! I'm not going to prove any theorems about that.... they are in here:

* André Joyal and Ross Street, [The geometry of tensor calculus I](https://www.sciencedirect.com/science/article/pii/000187089190003P).

> >**Puzzle 284.** Using the cap and cup, any morphism \\(f \colon x \to y \\) in a compact closed category gives rise to a morphism from \\(y^\ast\\) to \\(x^\ast\\). This amounts to 'turning \\(f\\) around' in a certain sense, and we call this morphism \\(f^\ast \colon y^\ast \to x^\ast \\). Write down a formula for \\(f^\ast\\) and also draw it as a string diagram.

> \\(y^\ast \stackrel{\sim}{\to} y^\ast \otimes I \stackrel{1_y \otimes \cap_x}{\to} y^\ast \otimes (x \otimes x^\ast) \stackrel{1_y \otimes (f \otimes 1_x)}{\to} y^\ast \otimes (y \otimes x^\ast) \stackrel{\sim}{\to} (y^\ast \otimes y) \otimes x^\ast \stackrel{\cup_y \otimes 1_x}{\to} I \otimes x^\ast \stackrel{\sim}{\to} x^\ast\\)

> ![function_cap_cup](http://aether.co.kr/images/function_cap_cup.svg)

This looks great! We take

\[ f \colon x \to y ,\]

use a cup to bend its output wire so that the output \\(y\\) becomes the input \\(y^\ast\\), use a cap to bend its input wire so that the input \\(x\\) becomes the output \\(x^\ast\\), and get a morphism we define to be

\[ f^\ast \colon y^\ast \to x^\ast .\]

> So the composite function...

You mean "composite morphism"...

> ...would be \\( f^\ast = (1_y \otimes \cap_x)(1_y \otimes f \otimes 1_x)(\cup_y \otimes 1_x)\\).

This simplified formula is only correct if you're in a _strict_ monoidal category. In your detailed formula

\\(y^\ast \stackrel{\sim}{\to} y^\ast \otimes I \stackrel{1_y \otimes \cap_x}{\to} y^\ast \otimes (x \otimes x^\ast) \stackrel{1_y \otimes (f \otimes 1_x)}{\to} y^\ast \otimes (y \otimes x^\ast) \stackrel{\sim}{\to} (y^\ast \otimes y) \otimes x^\ast \stackrel{\cup_y \otimes 1_x}{\to} I \otimes x^\ast \stackrel{\sim}{\to} x^\ast\\)

you've got some isomorphisms! First you've got the inverse of the right unitor:

\[ \rho_{y^\ast} \colon y^\ast \stackrel{\sim}{\to} y^\ast \otimes I \]

then the inverse of the associator:

\[ \alpha_{y^\ast, y, x^\ast} \colon y^\ast \otimes (y \otimes x^\ast) \stackrel{\sim}{\to} (y^\ast \otimes y) \]

and then the left unitor:

\[ \lambda_{x^\ast} \colon I \otimes x^\ast \stackrel{\sim}{\to} x^\ast \]

In a _strict_ monoidal category these are all identity morphisms. Also, in a strict monoidal category we can write \\(1_y \otimes (f \otimes 1_x)\\) as \\(1_y \otimes f \otimes 1_x \\) since the tensor product is associative. So, if our compact closed category is strict monoidal we can write:

\[ f^\ast = (1_y \otimes \cap_x)(1_y \otimes f \otimes 1_x)(\cup_y \otimes 1_x) .\]

In general, the formula is more complicated. This is one reason string diagrams are convenient: they allow us to hide the associators and unitors. Of course, it takes work to justify the use of string diagrams! I'm not going to prove any theorems about that.... they are in here:

* André Joyal and Ross Street, [The geometry of tensor calculus I](https://www.sciencedirect.com/science/article/pii/000187089190003P).