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

[Martin Escardo]

On 01/07/13 22:43, Guillaume Brunerie wrote:
> On 2013/7/1 Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>> 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).

Actually, I didn't mean what I wrote. I meant that U_omega should 
contain U_0, U_1, U_2, ... and more generally U_{sup f} should contain 
U_{f i} (not be equal to the union as I said), for cumulativity.


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

Well, this is the opposite of the expectation I expressed. It would be 
nice if the issues turn out to be orthogonal.

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

I mean: in the system you have, there is nothing to say that zero /= 
succ zero, for example. There is also no induction on Level. Although 
you hinted the possibility of adding this as a higher-inductive type. 
All this has to be formally explained if you want to formally argue that 
the system with a type of levels is a faithful extension of the system 
with constants for levels.

Martin


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