代数类型论与论域层次
Algebraic Type Theory and Universe Hierarchies
摘要：
人们普遍认为，类型论的代数概念只支持塔斯基式的宇宙，而罗素式的宇宙必须通过详细阐述而被删除。我们澄清的事态，回顾的细节Cartmell的纪律_广义代数理论_，展示了如何制定一个代数版本的Coquand的累积CWFS与宇宙的罗素。为了证明代数技巧的力量，我们用一个纯代数的方法证明了马丁-勒夫类型论的规范性，其中包含了论域、依赖函数类型和一个有两个常数的基类型。
英文摘要：
It is commonly believed that algebraic notions of type theory support only universes à la Tarski, and that universes à la Russell must be removed by elaboration. We clarify the state of affairs, recalling the details of Cartmell's discipline of _generalized algebraic theory_, showing how to formulate an algebraic version of Coquand's cumulative cwfs with universes à la Russell. To demonstrate the power of algebraic techniques, we sketch a purely algebraic proof of canonicity for Martin-Löf Type Theory with universes, dependent function types, and a base type with two constants.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
