[TYPES] Transfinite universe levels

[Stefan Monnier]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


Most type theory-based tools nowadays are based on a calculus with an
infinite hierarchy of predicative universes.  Some of them, such as
Agda, also allow abstraction over those levels, so we end up with a PTS
along the lines of:

    ℓ ::= z | s ℓ | ℓ₁ ∪ ℓ₂ | l      (where `l` is a level variable)

    S = { Type ℓ, Type ω, SortLevel }
    A = { Type ℓ : Type (ℓ + 1), TypeLevel : SortLevel }
    R = { (Type ℓ₁, Type ℓ₂, Type (ℓ₁ ∪ ℓ₂)),
          (SortLevel, Type ℓ, Type ω),
          (SortLevel, Type ω, Type ω) }

I was wondering if there's been work to push this to larger ordinals, to
allow maybe rules like

          (Type ω, Type ω, Type (ω·ω))

I.e. "deep universe polymorphism"


        Stefan