[Agda] How does level polymorphism fit into a valid type theory?
(from "More universe polymorphism")
Guillaume Brunerie
guillaume.brunerie at gmail.com
Sun Jun 30 15:54:43 CEST 2013
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
More information about the Agda
mailing list