论文标题
具有明确宇宙多态性的类型理论（修订和扩展版本）
Type Theory with Explicit Universe Polymorphism (revised and extended version)
论文作者
论文摘要
本文的目的是完善和扩展Sozeau和Tabareau的提议，以及Voevodsky在类型理论中为宇宙多态性的提案。在这些系统中，判断可以取决于宇宙级别之间的明确约束。我们在这里提出了一个系统，其中还拥有按宇宙级别和约束条件索引的产品。我们的理论对内部宇宙级别有判断，该宇宙级别是由后继操作和二进制超级操作的水平变量构建的，并且还判断了宇宙水平平等的判断。
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels.
