*-Autonomous Envelopes and Conservativity

Michael Shulman
(University of San Diego)

We prove 2-categorical conservativity for any {0,T}-free fragment of MALL over its corresponding intuitionistic version: that is, that the universal map from a closed symmetric monoidal category to the *-autonomous category that it freely generates is fully faithful, and similarly for other doctrines. This implies that linear logics and graphical calculi for *-autonomous categories can also be interpreted canonically in closed symmetric monoidal categories.

In particular, every closed symmetric monoidal category can be fully embedded in a *-autonomous category, preserving both tensor products and internal-homs. 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 Hyland–Schalk double gluing and a technique of Lafont. The same is true for other fragments of *-autonomous structure, such as linear distributivity, and the embedding can be enhanced to preserve any desired family of nonempty limits and colimits.

In Ugo Dal Lago and Valeria de Paiva: Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity&TLLA 2020), Online, 29-30 June 2020, Electronic Proceedings in Theoretical Computer Science 353, pp. 175–194.
Published: 30th December 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.353.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org