The inclusion $U$ of the (2,1)-category of symmetric monoidal categories with duals into the (2,1)-category of symmetric monoidal categories admits a left 2-adjoint functor $L$ for formal reasons.

In particular, for any symmetric monoidal category $C$, the unit map $C→L(C)$ exhibits $L(C)$ as the free symmetric monoidal category with duals generated by $C$.

Is there a citeable reference for any explicit construction of $L(C)$?

Generally speaking, we cannot expect the resulting functor $C→L(C)$ to be full, since the (formal) trace in $L(C)$ of a morphism in $C$ can give an endomorphism of the monoidal unit in $L(C)$ that does not come from $C$.

It seems to me that in the case when $C$ is a symmetric monoidal groupoid, it is reasonable to expect that the functor $C→L(C)$ is at least a faithful functor. Has this been shown explicitly?

**What conditions on $C$ guarantee that $C→L(C)$ is a faithful functor?**

I am particularly interested in the cases when $C$ is some symmetric monoidal category of infinite-dimensional vector spaces, such as Banach, Hilbert, or Fréchet topological vector spaces (possibly with invertible or unitary maps as morphisms), or (perhaps) solid modules over real numbers.

In the nonsymmetric case, the work of Delpeuch (Autonomization of monoidal categories) does give such an explicit construction of $L(C)$ and it proves that the inclusion functor $C→L(C)$ is a fully faithful strong monoidal functor, but this result does not seem to immediately extend to the symmetric case.

The forgetful functor $U$ factors through the (2,1)-category of traced symmetric monoidal categories, and the left adjoint functor from traced symmetric monoidal categories to symmetric monoidal categories with duals is given by the Int-construction of Joyal–Street–Verity (Traced monoidal categories, Section 4), who prove that the unit of this adjunction is a fully faithful strong monoidal functor.

However, I could not find any sources about free traced symmetric monoidal categories on symmetric monoidal categories, including conditions under which the unit map can be shown to be a faithful functor.