Left duality is a contravariant antimonoidal functor

Expanding the definition from [L1] with $f=1_X$ and then straightening the resulting coevaluation-evaluation pair by the zig-zag identities shows $(1_X{)}^{\vee }=1_{X^{\vee }}$.

The usual tensoring of the chosen dual pairs gives evaluation and coevaluation maps exhibiting $Y^{\vee }\otimes X^{\vee }$ as a left dual of $X\otimes Y$. Since $(X\otimes Y{)}^{\vee }$ is the chosen left dual of the same object, [L3] gives a unique compatible isomorphism $(X\otimes Y{)}^{\vee }\cong Y^{\vee }\otimes X^{\vee }\mathrm{.}$

For morphisms $X\stackrel{f}{\to }Y\stackrel{g}{\to }Z$, the defining composite for $(g\circ f{)}^{\vee }$ contains the block $g\circ f$ between one coevaluation and one evaluation. Splitting that block into $g$ followed by $f$ yields exactly the composite for $f^{\vee }\circ g^{\vee }$, so $(g\circ f{)}^{\vee }=f^{\vee }\circ g^{\vee }$. Hence $(-{)}^{\vee }$ is contravariant.

By [L4], the tensor unit $\mathbf{1}$ is itself a left dual of $\mathbf{1}$. Applying [L3] to the chosen left dual ${\mathbf{1}}^{\vee }$ and this canonical one gives a unique compatible isomorphism ${\mathbf{1}}^{\vee }\cong \mathbf{1}$. Together with step 1.2, this supplies the unit comparison, so $(-{)}^{\vee }$ is antimonoidal.