[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
