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

[Martin Escardo]

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
>