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

[Bas Spitters]

Vladimir is working on an ambitious new type system with separate
variables for universe levels.

http://uf-ias-2012.wikispaces.com/file/detail/Universe+polymorphic+type+sytem.pdf

On Tue, Jul 2, 2013 at 12:29 AM, Guillaume Brunerie
<guillaume.brunerie at gmail.com> wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda