[Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")

[Martin Escardo]

On 01/07/13 20:16, Guillaume Brunerie wrote:
> Well, if you want to define a polymorphic function (polymorphic on all
> small types, not restricted to some universe), you have to quantify
> over all levels.
> Or you can use typical ambiguity,

I don't think this should be an "either or" situation. One should have 
an explicit understanding of what universes and levels are, and typical 
ambiguity should be a shorthand for making types and terms readable 
(very much like implicit-argument notation) by erasing levels that can 
be automatically inferred.

> but this is kind of cheating.

It doesn't need to be.

> Maybe you could instead have a notion of universal quantification over
> all universes which would be a primitive notion, distinct from the
> usual Pi types.

It is sort of what you are doing, except that you quantify over indices. 
I find it slightly disturbing that the indices come with unspecified 
operations that "we know what they are" but we don't actually specify in 
the language.

> Various people were talking about that at the IAS this
> year but I don’t know if anyone tried to write down the rules.

Wouldn't they be very much like what you wrote for universe indices? 
Also, for cumulativity you probably need more than what you wrote: 
Somehow you have to express that U_{sup f} is the union of U_{f i} in 
your rules, don't you? Also, different zero-succ-sup expressions could 
give different indices for the same universe (very unlikely in a 
definitional way), and you can't talk about this in the type system you 
propose, at least not at the moment as it is presented (does it matter?).

> But if having a type of universe levels is consistent and natural and
> pretty, I don’t see why we should try to avoid it.

Perhaps. But, for example, if giving computational meaning to function 
extensionality, univalence, and higher-order inductive types is already 
difficult, it is going to be no easier with first-class-citizen, 
transfinite universe indices.

Moreover, I think it is nice to structure type theory in increasing 
levels of generality. For example, the theory can be defined without any 
universe. Then one can add one universe, then countably many universes, 
where the indices are meta-linguistic (this is the way I read the brief 
discussion about sequences of universes by Martin-Loef). If you 
incorporate the indices as a type, I would prefer to be able to see the 
previous system as naturally incorporated there. If you have a type of 
levels, you will have to explain how the meta-language natural-number 
indices live inside the object-language type of levels, to begin with.

So I am not sure (at least not yet) whether this is really "natural". We 
can decide whether it is pretty when we see all the details written down.

Is there an algorithm for typical ambiguity for the transfinite 
generalization of levels? Does it matter? Does this even make sense?

Best,
Martin