\mu {\circ}(a^* {\ensuremath{\otimes}}{\ensuremath{\mathrm{id}_{}}}) 
  = (a^\dag {\ensuremath{\otimes}}{\ensuremath{\mathrm{id}_{}}}) {\circ}\mu^\dag; \tag{H}\end{aligned}$$ or diagrammatically: $${
 \begin{tikzpicture}[scale=0.5]  \PandocStartInclude{tikz/H-lhs.tikz}\PandocEndInclude{input}{24}{23} \end{tikzpicture}}
  \; \stackrel{\text{(H)}}{=} \;
  {
 \begin{tikzpicture}[scale=0.5]  \PandocStartInclude{tikz/H-rhs.tikz}\PandocEndInclude{input}{24}{23} \end{tikzpicture}}.$$ Thus $a \mapsto a^*$ is indeed a ‘transfer of variables’.

Relationships between axioms (F) and (H)
----------------------------------------

The rest of this section compares axioms (F) and (H) at the abstract level of monoidal dagger categories. The following observation by Coecke, Pavlovi[ć]{} and Vicary is the central idea in their proof of Theorem \[cpvth\].

\[lem:cpv\] In any dagger monoidal category, (F) and (U) imply (H).

Define $a^* = (a^\dag {\ensuremath{\otimes}}{\ensuremath{\mathrm{id}_{}}}) {\circ}\delta {\circ}\varepsilon^\dag$. $${
 \begin{tikzpicture}[]  \PandocStartInclude{tikz/FUimplyH-1.tikz}\PandocEndInclude{input}{24}{23} \end{tikzpicture}}  \;=\;  {
 \begin{tikzpicture}[]  \PandocStartInclude{tikz/FUimplyH-2.tikz}\PandocEndInclude{input}{24}{23} \end{tikzpicture}}$$ This indeed satisfies (H). $${
 \begin{tikzpicture}[]  \PandocStartInclude{tikz/FUimplyH-3.tikz}\PandocEndInclude{input}{24}{23} \end{tikzpicture}}
    \; = \;
    {
 \begin{tikzpicture}[]  \PandocStartInclude{tikz/FUimplyH-4.tikz}\PandocEndInclude{input}{24}{23} \end{tikzpicture}}
    \; \stackrel{\text{(F)}}{=} \;
    {
 \begin{tikzpicture}[]  \PandocStartInclude{tikz/FUimplyH-5.tikz}\PandocEndInclude{input}{24}{23} \end{tikzpicture}}
    \; \stackrel{\text{(U)}}{=} \;
    {
 \begin{tikzpicture}[]  \PandocStartInclude{tikz/FUimplyH-6.tikz}\PandocEndInclude{input}{24}{23} \end{tikzpicture}}$$

Recall that a category is *monoidally well-pointed* if the following holds: $$\begin{aligned}
 f = g \colon A {\ensuremath{\otimes}}A' \to B {\ensuremath{\otimes}}B' 
  \;\;\; \Longleftrightarrow \;\;\; 
  \forall x \colon I \to A, y \colon I \to A' .\,\,f {\circ}(x {\ensuremath{\otimes}}y) = g {\circ}(x {\ensuremath{\otimes}}y).\end{aligned}$$ All the categories listed in our Examples are monoidally well-pointed in this sense.

\[lem:HAWPimplyF\] In a monoidally well-pointed dagger monoidal category, (H) and (A) imply (F).

For any 