广义论域体系与第一类论域能级
Generalized Universe Hierarchies and First-Class Universe Levels
摘要：
在类型论中，论域层次通常用于增加理论的表达能力，同时避免因大小问题而产生的不一致。有许多方法来指定论域层次，理论可能在累积性的细节、论域层次的选择、类型形成器和消除器的规范以及层次上可用的内部操作方面有所不同。在目前的工作中，我们的目标是提供一个框架，涵盖了很大一部分的设计空间。首先，我们开发的语法和语义的累积宇宙层次结构，层次可能来自任何一组配备了一个传递良基排序。在语义上，我们表明，归纳递归可以用来建模超限层次，也支持提升操作的类型代码，严格保持类型former。然后，我们考虑一个设置，其中宇宙水平是第一类类型，并受到任意的内部推理。这概括了Coq的有界多态性特征，同时也概括了Agda的内部层次计算。
英文摘要：
In type theories, universe hierarchies are commonly used to increase the expressive power of the theory while avoiding inconsistencies arising from size issues. There are numerous ways to specify universe hierarchies, and theories may differ in details of cumulativity, choice of universe levels, specification of type formers and eliminators, and available internal operations on levels. In the current work, we aim to provide a framework which covers a large part of the design space. First, we develop syntax and semantics for cumulative universe hierarchies, where levels may come from any set equipped with a transitive well-founded ordering. In the semantics, we show that induction-recursion can be used to model transfinite hierarchies, and also support lifting operations on type codes which strictly preserve type formers. Then, we consider a setup where universe levels are first-class types and subject to arbitrary internal reasoning. This generalizes the bounded polymorphism features of Coq and at the same time the internal level computations in Agda.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
