A.2.3 Type universes
We postulate an infinite
hierarchy of type universes
Each universe is contained in the next, and any type in is also in :
{mathpar}
\inferrule*[right=-intro]
ΞΒ
Ξ β’ _i : _i+1
\inferrule*[right=-cumul]
Ξ β’A : _i
Ξ β’A : _i+1
We shall set up the rules of type theory in such a way that
implies for some . In other words, if plays the role of a type then it is in some universe. Another property of our type system is that
implies and .
Title | A.2.3 Type universes |
---|---|
\metatable |