A.1.1 Type universes

We postulateMathworldPlanetmath a hierarchy of universesPlanetmathPlanetmath denoted by primitive constants


The first two rules for universes say that they form a cumulative hierarchy of types:

  • β€’

    𝒰m:𝒰n for m<n,

  • β€’

    if A:𝒰m and m≀n, then A:𝒰n,

and the third expresses the idea that an object of a universe can serve as a type and stand to the right of a colon in judgments:

  • β€’

    if Ξ“βŠ’A:𝒰n, and x is a new variable,11By β€œnew” we mean that it does not appear in Ξ“ or A. then ⊒(Ξ“,x:A)𝖼𝗍𝗑.

In the body of the book, an equality judgment A≑B:𝒰n between types A and B is usually abbreviated to A≑B. This is an instance of typical ambiguity, as we can always switch to a larger universe, which however does not affect the validity of the judgment.

The following conversion rule allows us to replace a type by one equal to it in a typing judgment:

  • β€’

    if a:A and A≑B then a:B.

Title A.1.1 Type universes