Type Theories with Universe Level Judgements

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.