You find yourself, like Jacob, gazing up the rungs (for me, ropes)

of a ladder that seems to have constructed itself

to avoid leaving you flat on the ground.

But what, you ask, in the arching presence of the angels,

do you do at the top?

Type theories, to be consistent, cannot be uniform. Somewhere, your power must ebb, abstractions diminish, until finally you are left with the beautiful silence of a single symbol (maybe ). Type : type is also beautiful, but long known to be inconsistent: collapsing everything to one level ruins your type theory as a logic. There are more subtle examples of the need to give up your power as you ascend (this starts to sound like John of the Cross). You cannot repeat impredicative quantification one level up, for example: Girard proved this is paradoxical in his dissertation. So if you are an impredicativist as I am, your kind level must be strictly weaker than your type level.

But what about if you are a predicativist, perhaps a devotee (as I also am) of Agda? Agda, and also Coq via its ECC (Extended Calculus of Constructions, of Zhaohui Luo) structure, seem to avoid this quietist imperative I am mentioning. Above the current level, there is another, with essentially the same power. And beyond that, another, ad infinitum. The ladder goes up forever! We surpass the heavens!

But no, experienced Agda and Coq users know that is sadly not what happens. Much like the tower of Babel, the predicative universe hierarchy does not satisfy the desires of abstraction. For some constructions make sense at all levels, and hence we introduce the seductive ideas of typical ambiguity (considered for a system of Coquand’s which is a predecessor of ECC, by Harper and Pollack) and universe polymorphism (also considered by Harper and Pollack). Universe polymorphism as I understood it from Agda seems a bit different from what Harper and Pollack propose. And it seems that typical ambiguity is found more in Coq than Agda. (I could be wrong on these points!) In Agda, there seems to be the curious idea that we can quantify over all levels of the hierarchy explicitly. And we are then left with the conundrum of what level such a quantification itself has? Of course, for soundness reasons, it cannot have one of the levels covered by the level quantification. So we have to make up a new level, namely . And we see that level quantification was a charade to begin with: we are definitely **not** quantifying over all the levels, just some prefix of them. And it seems Agda does not make available to you to use in your code. So this just seems very hacky.

More principled is something that I think is closer to the kind of universe polymorphism that Harper and Pollack were proposing, which in their work is located at global definitions (not arbitrary terms). And this is the answer to my riddle at the beginning: when you reach the top of your ladder, you have to “go meta”. It is a beautiful insight that we can internalize the induction scheme one finds in Peano Arithmetic as a single second-order axiom. We have passed from the meta-level, with a family of formulas, to a single object-language formula. I propose that when we reach the top layer of our layered type theory, we do the reverse. We add schematic definitions.

Here at Iowa, we are working on this new Cedille type theory and system. Some of my recent papers are about this. There, we have a predicative hierarchy truncated at level 2. Ha! There are just terms, types, and kinds. It is actually more convenient to reach the end of the ladder faster! And going schematic means that while we do not support kind-level functions, we will allow you to define parametrized kinds. So you can give a top-level definition of some kind parametrized by terms or types. The definition itself does not need some funny type with level or some additional superkind structure. Of course, one can only use the definition with all parameters instantiated.

Simple, but extends expressivity a bit just out of the reach of what can be internalized in the theory.

## 2 Comments

I believe that we could give a type to universe-polymorphic definition indeed, the ordinal omega, and continue a predicative hierarchy with higher ordinals to keep giving types to these types (omega + 1, etc.) — then the bounds would be on the limits of the ordinal notation system you choose. I suppose that the reason why no one has gotten around to implement this is that they have not felt the need — predicativity will always find a way to be limiting in any case.

I am not completely sure what difference you are making between “an inhabitant at a type that does not itself have a kind in the system” and “a schematic inhabitant that can only be used fully-applied”. The latter seems to be a somewhat restriction of the former, that will have a similar effect by preventing you from using the term in any typing rule that requires its type to be kindable (such as passing it, unapplied, to a polymorphic function).

Yes, we can pick a system of ordinal notations and use that for indexing the universe hierarchy. But this will never satisfy anyone because what they really want is impredicative quantification. 🙂 They want to quantify over *all* levels, which cannot be done predicatively. Also, it should be clear that the tail will be wagging the dog at that point.

I am comparing two different ways of extending the system past what is really allowed by the level structure of the type theory. The Agda way, where we allow quantification over (supposedly) all universe levels, but cannot then assign a type to such quantifications from among the types that users can include in their programs. And this alternative extension, where we allow parametrized definitions at the highest level of the system. The latter is more principled, in my opinion, though does not pretend (as indeed the former *pretends*) to give you some kind of polymorphism across levels. It just lets you creep towards another level, without actually adding one.