论文标题
* - 自主的信封和保守性
*-Autonomous Envelopes and Conservativity
论文作者
论文摘要
对于任何{0，t}的片段，我们在其相应的直觉版本上证明了2类的保守性：也就是说，它是从封闭的对称单类类别到 * - 自治类别的通用映射，它自由地生成了完全忠实的，并且对其他教义类似。这意味着 * - 自主类别的线性逻辑和图形分解也可以在封闭的对称单体类别中进行规范解释。 特别是，每个闭合的对称单类别类别都可以完全嵌入 *自主类别中，从而保留张量和内部单体。 实际上，我们首先用Yoneda风格的嵌入（增强的“ Hyland Invelope”（可以被视为日间卷积的多种类别形式）直接证明这一点，然后从Hyland-Schalk Double Gluing和LaFont技术中推断出2个保存。 对于 *自主结构（例如线性分布）和嵌入的其他片段也可以增强以保留任何所需的非空限制和colimits家族。
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.
