The aim of this paper is to refine and extend Voevodsky's draft "A universe polymorphic type system" that outlines a type theory where judgments can depend on equalities between universe levels expressions (constraints). We first recall a version of type theory with an externally indexed sequence of universes. We then add 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. Furthermore, we extend this type theory with rules for level-indexed product types. Finally, we add constraints to the theory, so that a hypothetical judgment can depend on equalities between universe levels. We also give rules for constraint-indexed product types, and compare the resulting type theory to Voevodsky's.

翻译：本文的目的是完善和扩展Voevodsky的“ 宇宙多元形态系统” 草案, 该草案概述了一种类型的理论, 判断可以取决于宇宙水平表达式( 约束性) 之间的等同性。 我们首先回顾一个版本的类型理论, 带有外部指数化的宇宙序列 。 然后我们加上对内部宇宙水平的判断, 由水平变量建立, 由后续操作和二进制顶峰操作建立, 以及宇宙水平平等性判断。 此外, 我们扩展了这种类型理论, 并增加了水平指数化产品类型的规则 。 最后, 我们增加了对理论的限制, 这样假设性判断可以取决于宇宙水平的等同性 。 我们还给出了限制指数化产品类型的规则, 并将由此产生的类型理论与Voevodsky 相比较 。