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

[Guillaume Brunerie]

> Ok, I understand, Guillaume. The crucial thing, in your formulation
> below of transfinite universes, is that Level is a type but cannot
> live in a universe, right? (So it doesn't have a type.)

Yes, in order to have transfinite levels, the type Level cannot live
in any universe or the type theory would be inconsistent.

> By the way, have you see this? http://www2.math.uu.se/~palmgren/universe.pdf

Yes, I’ve seen it. It’s quite similar but stronger because he assumes
the existence of a super-universe which is a universe containing
itself "transfinitely many" smaller universes. I think that in my
formulation, the collection of all types corresponds basically to the
types in Palmgren’s superuniverse (also the presentation is different,
he’s not indexing the universes by levels but directly by some family
of types it should contain).

> (In the IAS HoTT mailing list, T. Coquand posted a cumulative
> system with judgements Type_n for every n (27 Feb this year,
> with subject "Russell and Tarski"). But every type does live in
> a universe, and the levels n are in the meta-language.)

That’s different, he’s explaining a way to manage universes in between
Russel and Tarski universes. But that’s interesting, thank you for
reminding me of it, I somehow missed it when he sent it.

Guillaume

2013/7/1 Martin Escardo <m.escardo at cs.bham.ac.uk>:
> Ok, I understand, Guillaume. The crucial thing, in your formulation below of
> transfinite universes, is that Level is a type but cannot live in a
> universe, right? (So it doesn't have a type.)
>
> By the way, have you see this? http://www2.math.uu.se/~palmgren/universe.pdf
>
> (In the IAS HoTT mailing list, T. Coquand posted a cumulative system with
> judgements Type_n for every n (27 Feb this year, with subject "Russell and
> Tarski"). But every type does live in a universe, and the levels n are in
> the meta-language.)
>
> Best,
> Martin
>
>
> On 30/06/13 14:54, Guillaume Brunerie wrote:
>>
>> I will describe a type theory with infinitely many universes (à la
>> Russel), and explicit universe polymorphism with a type of universe
>> level (this is basically what Agda does)
>>
>> There are two basic judgments:
>>
>> A  type
>> a : A
>>
>> Note that unlike in Coq, the first judgment is not a special case of the
>> second one, a valid type need not be a valid term.
>> The possible expressions are the following:
>>
>> Level, zero, succ, max, Set i,
>> (x : A) -> B(x), lambda x -> u(x), u v
>>
>> The typing rules are the following
>>
>> * Universe levels:
>>
>> Level : Set zero
>> zero : Level
>> succ : Level -> Level
>> max : Level -> Level -> Level
>>
>> * Universes:
>>
>> i : Level
>> ----------
>> Set i : Set (succ i)
>>
>> A : Set i
>> ----------
>> A  type
>>
>> A : Set i
>> ---------- (cumulativity, optional, not present in Agda)
>> A : Set (succ i)
>>
>> * Pi formation (there are two formation rules, one for arbitrary types
>> and one for small types):
>>
>> A  type
>> x : A |- B(x)  type
>> ----------
>> (x : A) -> B(x)  type
>>
>> i j : Level
>> A : Set i
>> x : A |- B(x) : Set j
>> ----------
>> (x : A) -> B(x) : Set (max i j)
>>
>> * Pi introduction, elimination and computation:
>>
>> As usual (and (x : A) -> B(x) is not required to small)
>>
>> *****
>>
>> For the transfinite version, you replace "Level : Set zero" by "Level
>> type", change max to sup with the appropriate typing rule and change the
>> second Pi formation rule by one where j can depend on x and where the
>> universe level is computed with sup.
>>
>> Note that (in the first version) in order to have a small Pi-type, the
>> codomain is required to be of a uniform universe level, in particular a
>> valid type like (i : Level) -> Set i is not a valid term.
>> In the transfinite version, this requirement is dropped, any Pi between
>> small types is small even if the codomain is not of a uniform universe
>> level. But on the other hand the type of universe levels is now big, so
>> (i : Level) -> Set i is still not a valid term (and still a valid type).
>> And in the transfinite version, (n : Nat) -> Set (Nat-to-Level n) is
>> small and of type Set omega (and you can define Nat-to-Level because you
>> have large elimination), but it's big in the first version.
>>
>> I also already sketched the set-theoretic semantics of both versions in
>> some previous email, so it seems consistent.
>>
>> Best,
>> Guillaume
>>
>> Le 30 juin 2013 14:02, "Darryl McAdams" <psygnisfive at yahoo.com
>> <mailto:psygnisfive at yahoo.com>> a écrit :
>>
>>
>>     It was mentioned in the referenced thread that types like
>>
>>          {i : Level} -> {A : Set l} -> A -> A
>>
>>     do not themselves have types. Even with transfinite levels it
>>     couldn't be typed, because i would be instantiated to any level,
>>     including transfinite ones. How does level polymorphism get handled
>>     in a consistent type theory, if at all? Not just Agda's underlying
>>     type theory, but any type theory in general?
>>     - Darryl McAdams
>>
>>     _______________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto: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