Predicative type hierarchy

[atennapel]

What would be the simplest way to go from the inconsistent Type : Type to the consistent Type0 : Type1 : TypeN?
Adding the predicative hierarchy is not so difficult, but making it more usable would require either cumulativity or polymorphism.

Cumulativity

The simplest seems to me to add a lifting operator:

e : Type m
---------------------
^n e : Type (m + n)

Actually I have the feeling you'd need two operators, one for values and another for types. I've heard that this lifting operator is actually quite tricky to implement in combination with NbE.

Polymorphism

Adding universe polymorphism like Agda seems quite easy since you can piggyback on the existing inference system. On the other hand Agda apparently has a solver for the universes and lifting operators as well, so it might turn out to be more involved.

So which approach do you think will be simplest to make the system consistent?

[AndrasKovacs]

• Lifting is not cumulativity. Cumulativity in practice, e.g. as in Coq, means that A : Type n implies A : Type m for n < m without any lifting operation required in the surface language.
• Lifting and polymorphism are orthogonal, there's no need to choose one.

The absolute simplest solution is to have a built-in lifting operator, such that Lift A : Type (suc i) when A : Type i, and every type former stays in the same level, so A -> B : Type i iff A : Type i and B : Type i. Also, there's lift and unlift for terms, which is a definitional isomorphism between A and Lift A. But there are no other computation rules. Note that even in this setup we need universe metas, because e.g. inferring a type for a hole requires an unknown universe. But we only need unification for strict equality of levels, we don't need to reason about maxima or ordering.

This can upgraded by saying that Lift and lift compute on structure of type and term formers. For example, Lift (A -> B) = Lift A -> Lift B, and lift (\x -> t) = \x -> lift (t (unlift x)). This can be convenient, because lifting computes out of the way of more interesting constructions. To my knowledge this hasn't been used anywhere at scale, so your mileage may vary.

Another direction of upgrade is to introduce maxima of levels, and have type formers return in such levels. This makes many instances of lifting unnecessary. However, it also requires slightly stronger level unification. This is used in Agda.

Universe polymorphism has numerous different versions. The simplest is when

• Levels can only depend on levels
• There is no type of levels
• Level-polymorphic types are not in any universe

Agda is more complicated, because there is a type of levels in Set0, hence, levels can depend on any data.

The strongest version that I know of has the following features:

• Not only levels are internal, but their ordering relation as well.
• Level-polymorphism is a special case of dependent functions with bounded levels as arguments.
• There are internal eliminators both for levels and their ordering. So we can write a function Level -> Nat, while in Agda we can only write Nat -> Level.

I don't think such "fully internal" levels have been implemented anywhere. I did a tiny sketch for their semantics here, a more detailed treatment is clearly needed, but I'm quite confident that it works.

I'm not too familiar with the implementation of cumulativity + polymorphism in Coq, I only know that it's significantly more complicated than in Agda.