In dependent type theory, being able to refer to a type universe as a term itself increases its expressive power, but requires mechanisms in place to prevent Girard's paradox from introducing logical inconsistency in the presence of type-in-type. The simplest mechanism is a hierarchy of universes indexed by a sequence of levels, typically the naturals. To improve reusability of definitions, they can be made level polymorphic, abstracting over level variables and adding a notion of level expressions. For even more expressive power, level expressions can be made first-class as terms themselves, and level polymorphism is subsumed by dependent functions quantifying over levels. Furthermore, bounded level polymorphism provides more expressivity by being able to explicitly state constraints on level variables. While semantics for first-class levels with constraints are known, syntax and typing rules have not been explicitly written down. Yet pinning down a well-behaved syntax is not trivial; there exist prior type theories with bounded level polymorphism that fail to satisfy subject reduction. In this work, we design an explicit syntax for a type theory with bounded first-class levels, parametrized over arbitrary well-founded sets of levels. We prove the metatheoretic properties of subject reduction, type safety, consistency, and canonicity, entirely mechanized from syntax to semantics in Lean.

翻译：在依赖类型理论中，能够将类型宇宙本身作为项来引用可增强其表达能力，但需要建立相应机制以防止在类型嵌套类型的情况下，吉拉尔悖论导致逻辑不一致性。最简单的机制是采用按层级序列（通常为自然数）索引的宇宙层级结构。为提高定义的可复用性，可将其设计为层级多态的，即对层级变量进行抽象并引入层级表达式的概念。为获得更强的表达能力，可将层级表达式本身作为一等项处理，此时层级多态性可归约为对层级进行量化的依赖函数。此外，有界层级多态通过能够显式声明层级变量的约束条件，提供了更强的表达能力。虽然具有约束的一等层级的语义已知，但其语法与类型规则尚未被明确表述。然而构建良行为的语法并非易事；先前存在的一些具有有界层级多态的类型理论未能满足主体归约性质。在本工作中，我们为具有有界一等层级的类型理论设计了显式语法，该语法可参数化任意良基的层级集合。我们在Lean中实现了从语法到语义的完整机械化证明，验证了主体归约、类型安全性、一致性和典范性等元理论性质。