[TYPES] Transfinite universe levels

[Philippa Cowderoy]

I've certainly meant to play with that! Especially for reflection 
purposes. Never actually did though, and I'd be interested to know if 
someone else has.


On 10/07/2018 22:50, Stefan Monnier wrote:
> [ 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