Reference for free symmetric monoidal categories with duals on symmetric monoidal categories 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.
 A: In my thesis (which should be posted soon) I formally deduce the existence of "$L_{\infty,1}$", in an $(\infty,1)$-categorical setting; I do not provide an explicit construction. One point I exploit in my thesis is that there are several variants of $L_{\infty,1}$, respecting additional colimits and so forth, which also exist and are sometimes more what one wants.
 I believe that $L_{2,1}C$ admits a description of the following form.

*

*Objects: pairs $(a_+,a_-) \in Ob C \times Ob C$


*Morphisms: $Hom((a_+,a_-), (b_+,b_-)) = \int^{x \in C} C(a_+ \otimes b_- \otimes x, b_+\otimes a_- \otimes x)$
(that's a coend in there.)

*

*To compose $f : a_+ \otimes b_- \otimes x \to b_+ \otimes a_- \otimes x$ with $g : b_+ \otimes c_- \otimes y \to c_+ \otimes b_- \otimes y$, you just compose along the common $b_+$ part (after tensoring with appropriate identities and inserting a few swaps) to get a map $a_+ \otimes c_-  \otimes (b_- \otimes x \otimes y) \to c_+ \otimes a_- \otimes (b_- \otimes x \otimes y)$
etc. The canonical functor $C \to L(C)$ sends $c$ to $(c,I)$ where $I$ is the unit, and the dual of $(c_+,c_-)$ is $(c_-,c_+)$.
If the above description is correct, perhaps you could find a faithfulness criterion using it. 
I am having difficulty convincing myself that any explicit construction along the above lines actually has duals for objects, if it is well-defined at all.
A: I thought the autonomization construction can be generalized to the symmetric case, and had a go at writing up the construction: https://arxiv.org/abs/2201.07527
However it does not work, because of an observation attributed to Plotkin:
http://ncatlab.org/nlab/show/traced+monoidal+category#adding_traces
Because compact closed categories are also traced, this means we cannot hope for a faithful injection in general.
