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

[Guillaume Brunerie]

I forgot to mention what Agda's Setomega means. I'm not familiar with
Agda's source code, so I'm mainly guessing.

In Agda there is only one judgement "a : A", but there is a special thing
called Setomega whose only possible use is at the right-hand side of a
colon, and the judgement "A : Setomega" in Agda means exactly the same
thing as my judgement "A  type".
Setomega is not a valid term and not even a valid type, you cannot consider
Setomega -> Setomega for instance. The only use of Setomega is to embed
easily the judgment "A  type" in Agda's source code where everything was
supposed to have a type before the introduction of universe polymorphisn.

Guillaume
Le 30 juin 2013 15:54, "Guillaume Brunerie" <guillaume.brunerie at gmail.com>
a écrit :

> 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/25587d70/attachment.html