语境理解的2-范畴分析
A 2-categorical analysis of context comprehension
AI总结：
本研究将语境理解的两种范畴模型的经典等价性推广到非离散情形，通过“项即余代数”的视角利用结构-语义伴随证明两类2-范畴的双等价性，并提供框架比较不同学者定义的结构态射。
摘要：
我们研究了类型论中语境理解操作的两种主要范畴模型——即P. Dybjer提出的带族范畴（categories with families）与B. Jacobs提出的理解范畴（comprehension categories）——之间的等价性，并将其推广到非离散情形。经典等价性可以用“项即截面”这一口号来概括。通过将“项视为余代数”，我们展示了如何利用结构-语义伴随来证明理解范畴的2-范畴与（非离散的）带族范畴的2-范畴是双等价的。该双等价在离散情形下可退化为Hofmann证明的经典等价性。它还提供了一个框架，用于比较文献中出现的、在相关结构的保持程度上存在差异的这些结构的不同态射。我们特别考察了Claraimbault-Dybjer、Jacobs、Larrea和Uemura定义的态射。
英文摘要：
We consider the equivalence between the two main categorical models for the type-theoretical operation of context comprehension, namely P. Dybjer's categories with families and B. Jacobs' comprehension categories, and generalise it to the non-discrete case. The classical equivalence can be summarised in the slogan: "terms as sections". By recognising "terms as coalgebras", we show how to use the structure-semantics adjunction to prove that a 2-category of comprehension categories is biequivalent to a 2-category of (non-discrete) categories with families. The biequivalence restricts to the classical one proved by Hofmann in the discrete case. It also provides a framework where to compare different morphisms of these structures that have appeared in the literature, varying on the degree of preservation of the relevant structure. We consider in particular morphisms defined by Claraimbault-Dybjer, Jacobs, Larrea, and Uemura.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
