依赖型理论的代数表示
Algebraic Presentations of Dependent Type Theories
摘要：
在本文中，我们提出了一个抽象的定义，依赖型理论本质上是代数理论。这个定义的主要优点之一是它的可组合性：简单的理论可以组合成更复杂的理论，并且所得到的理论的不同性质可以从基本理论的性质推导出来。我们定义一类代数依赖型理论，使我们不仅可以结合理论，但也考虑它们之间的等价关系。我们还研究了这些理论的模型，并表明人们可以把它们看作是具有附加结构的上下文范畴。
英文摘要：
In this paper, we propose an abstract definition of dependent type theories as essentially algebraic theories. One of the main advantages of this definition is its composability: simple theories can be combined into more complex ones, and different properties of the resulting theory may be deduced from properties of the basic ones. We define a category of algebraic dependent type theories which allows us not only to combine theories but also to consider equivalences between them. We also study models of such theories and show that one can think of them as contextual categories with additional structure.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
