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

[Guillaume Brunerie]

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> 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
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130630/3cbc58a9/attachment.html