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

[Guillaume Brunerie]

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

Ok. I actually didn’t give the rules for cumulativity because even if
cumulativity can be helpful, subtyping makes me uneasy and I would
prefer to avoid it.
But to have cumulativity one would say that for f : A -> Level, with A
: U_i, then U_{sup f} contains all U_{f a} for a : A and also U_i (the
sup f should really be understood as max(i,sup f)).

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

You can probably prove that zero ≠ succ zero (assuming you can apply
the identity type to the type of universe levels).
Indeed, if zero = succ zero, then you have U_zero : U_zero so you can
reproduce the paradox of Type : Type.

About induction on Level, I don’t know if this is something we would
want to have or not. But even if Level is a higher inductive type, I
don’t think we can use induction to prove zero ≠ succ zero given that
it’s not decidable whether some level is equal to zero or not.

Guillaume


>>> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda