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

[Guillaume Brunerie]

On 2013/7/1 Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>
> 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.

Is there a way to mix explicit universe polymorphism with typical
ambiguity? I only know Agda where there is no typical ambiguity at all
and Coq where everything is implicit.
If there is a way to have the benefits of both I would like to see it.

>> 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?

I think they were actively trying to avoid having a type of universe levels.

> 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?

Definitely not. For instance the function   (n : Nat) -> Set
(Nat-to-Level n)   lives in U_omega but not in any U_n, even if omega
= sup(n : Nat).
>From the point of view of large cardinals, you have [[ U_n ]] =
V_{\kappa_n}  where \kappa_n is the nth inaccessible cardinal and [[
U_omega ]] = V_{\kappa_omega}. But \kappa_omega is much bigger than
the sup of all \kappa_n (this sup is not inaccessible, it’s of
cofinality omega).

> 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?).

Yes, that’s a problem. I’m not sure when it matters but there is
definitely something missing here.
Maybe the type of universe levels should be defined as a higher
inductive type :-)

>> 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.

I think it’s a completely different problem. I would hope that if we
can give computational content to HoTT with ordinary universes on the
one hand, and to intentional type theory with transfinite universe
levels on the other hand, then giving computational content to HoTT
with transfinite universe levels is no harder.

> 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.

Well, the meta-language 0 corresponds to zero : Level, the
meta-language 1 corresponds to succ zero : Level, and so on.
I’m not sure I understood what you mean.

> 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.

Sure, this is very subjective.

> Is there an algorithm for typical ambiguity for the transfinite
> generalization of levels? Does it matter? Does this even make sense?
>
> Best,
> Martin
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda