A.2.3 Type universes

We postulateMathworldPlanetmath an infiniteMathworldPlanetmath hierarchy of type universesPlanetmathPlanetmath


Each universe is contained in the next, and any type in 𝒰i is also in 𝒰i+1: {mathpar} \inferrule*[right=𝒰-intro] Γ 𝖼𝗍𝗑 Ξ“ βŠ’π’° _i : 𝒰 _i+1 \inferrule*[right=𝒰-cumul] Ξ“ ⊒A : 𝒰 _i Ξ“ ⊒A : 𝒰 _i+1 We shall set up the rules of type theoryPlanetmathPlanetmath in such a way that Ξ“βŠ’a:A implies Ξ“βŠ’A:𝒰i for some i. In other words, if A plays the role of a type then it is in some universe. Another property of our type system is that Ξ“βŠ’a≑b:A implies Ξ“βŠ’a:A and Ξ“βŠ’b:A.

Title A.2.3 Type universes