autonomous envelopes Article Swipe
We show the doctrine of $\ast$-autonomous categories is 2-conservative over the doctrine of closed symmetric monoidal categories, i.e. the universal map from a closed symmetric monoidal category to the $\ast$-autonomous category that it freely generates is fully faithful. This implies that linear logics and graphical calculi for $\ast$-autonomous categories can also be interpreted canonically in closed symmetric monoidal categories. In particular, our result implies that every closed symmetric monoidal category can be fully embedded in a $\ast$-autonomous category, preserving both tensor products and internal-homs. But in fact we prove this directly first with a Yoneda-style embedding (an enhanced Hyland envelope that can be regarded as a polycategorical form of Day convolution), and deduce 2-conservativity afterwards from double gluing and a technique of Lafont. Since our method uses polycategories, it also applies to other fragments of $\ast$-autonomous structure, such as linear distributivity. It can also be enhanced to preserve any desired family of nonempty limits and colimits.
