局部次笛卡尔闭范畴
Locally subcartesian closed categories
浏览论文内容
中文总结 AI 辅助
该研究引入局部次笛卡尔闭范畴，发展其基本理论，扩展多项式理论，通过Lawvere quantale和名义集范畴举例说明，为外延依赖仿射类型理论提供了自然的范畴语义。
中文摘要 AI 辅助
我们引入局部次笛卡尔闭范畴：具有拉回的范畴，配备拉回子对象的连贯选择，使得所得仿射基变换函子有右伴随。我们发展基本理论，强调与局部笛卡尔闭范畴的类比，并通过证明每个切片范畴是幺半闭且投影联合单态来证明术语合理性。我们还扩展多项式理论，表明这样的范畴产生Street意义下的多项式双范畴，与次笛卡尔多项式函子的2 - 范畴双等价。我们用Lawvere quantale作为基本例子和名义集范畴作为更丰富的例子来说明该理论。这项工作为具有束上下文和仿射蕴含的外延依赖仿射类型理论提出了自然的范畴语义。
英文摘要
We introduce locally subcartesian closed categories: categories with pullbacks equipped with a coherent choice of subobjects of pullbacks, such that the resulting affine base-change functors have right adjoints. We develop the basic theory, emphasizing the analogy with locally cartesian closed categories, and justify the terminology by showing that every slice category is monoidal closed with jointly monic projections. We also extend the theory of polynomials, showing that such a category gives rise to a bicategory of polynomials in the sense of Street, biequivalent to a 2-category of subcartesian polynomial functors. We illustrate this theory with the Lawvere quantale as a basic example and the category of nominal sets as a richer one. This work suggests a natural categorical semantics for an extensional dependent affine type theory with bunched contexts and affine implication.
