Multiple Universe Hierarchies

Goals:

• Handle Prop/SProp/Type gracefully during elaboration, type-checking and extraction.
• Generalize universe handling to allow new, separate hierarchies, e.g. for effectful type theories
• Generalize universe polymorphism to sort polymorphism: allowing generic constructions that can be instantiated with Prop/SProp as well as predicative Types later on.

Difficulties:

• Notion of sort variable during elaboration
• How to distinguish typing constraints i < j coming from |- Type i : Type j and cumulativity constraints i <= j when i+1 <= j becomes i < j. Seems necessary to handle impredicativity correctly.
• Keeping sorts in terms, e.g changing bindings to x : T : s would make a more uniform system (e.g. erasure would only keep x : T : Set variables). Also avoids having a proof-relevant well-formedness judgement in the theoretical presentation (well-formedness currently includes a sorting of each type). This involves implementing and using a new sort-substitution function on terms once we can abstract on them, subsuming universe substitution.