  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.
