[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"


        Stefan


More information about the Types-list mailing list