一种带有显式宇宙多型的类型理论的通用代数理论
A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
AI总结：
本文提出两种类型理论的通用代数理论，用于抽象描述其高层结构，并探讨其与范畴逻辑和初始性猜想的相关性。
摘要：
我们提出了对应于我们论文中两种类型理论稍作修改版本的通用代数理论。我们首先提出了一种针对具有额外结构的范畴族的通用代数理论，对应于马丁-洛夫类型理论带有外部塔的宇宙。然后我们提出了一种针对具有额外结构的层级索引范畴族的通用代数理论，对应于马丁-洛夫类型理论中的显式宇宙多型：一种具有宇宙层级判断、内部索引宇宙和层级索引乘积的理论。通过这种方式，我们得到了这两种理论作为各自通用代数理论初始模型的抽象刻画。因此，我们从类型理论的语法和推导规则的细节中抽象出来，突出其高层结构。更广泛地说，本工作可以被视为基于通用代数理论和范畴族的范畴逻辑统一方法的案例研究。我们还讨论了其与沃伊诺夫斯基初始性猜想项目的相关性。
英文摘要：
We present generalized algebraic theories corresponding to slightly modified versions of two of the type theories in our paper Type Theory with Explicit Universe Polymorphism. We first present a generalized algebraic theory for categories with families with extra structure corresponding to Martin-Lof type theory with an external tower of universes. We then present a generalized algebraic theory for level-indexed categories with families with extra structure corresponding to Martin-Lof type theory with explicit universe polymorphism: a theory with universe level judgments, internally indexed universes, and level-indexed products. In this way we get abstract characterizations of the two theories as initial models of their respective generalized algebraic theories. We thus abstract from details of the grammar and inference rules of the type theories and highlight their high-level structure. More broadly, the present work can be viewed as a case study of a uniform approach to categorical logic based on generalized algebraic theories and categories with families. We also discuss the relevance to Voevodsky's initiality conjecture project.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
