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.

翻译：本文旨在精炼并扩展Sozeau与Tabareau以及Voevodsky关于类型论中宇宙多态性的方案。在这些系统中，判断可依赖于宇宙层级间的显式约束。我们在此提出一个系统，其中还引入了按宇宙层级和约束索引的乘积。我们的理论包含内部宇宙层级的判断（由层级变量通过后继运算和二元上确界运算构建），以及宇宙层级相等性判断。