[TYPES] Transfinite universe levels

Stefan Monnier monnier at IRO.UMontreal.CA
Tue Jul 10 17:50:11 EDT 2018

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"


More information about the Types-list mailing list