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

[Guillaume Brunerie]

On 2013/6/30 Darryl McAdams <psygnisfive at yahoo.com> wrote:
> Using type judgments like this suggests that there should be ways to have
> universe polymorphism but also allow "obnoxiously large" types like
>
>     ((i : Level) -> Set i) -> (i : Level) -> Set i

Yes. It doesn’t seem that problematic to me, that’s just a large type.
And I just tried, Agda accepts it.

> but wouldn't allow something like this:
>
>     id : {i : Level} {A : Set i} -> A -> A
>     id x = x
>
>     -- this should fail
>     id id : {i : Level} {A : Set i} -> A -> A
>
> because you can't get the judgment that the type of id is a Set i for some
> i, all you can get is that it's a type.

Yes. Actually, Agda accepts the following:

> id : {i : Level} {A : Set i} -> A -> A
> id x = x
>
> abc : {i : Level} {A : Set i} -> A -> A
> abc = id id

But the reason it works is because Agda introduces implicit lambda
abstractions for the implicit arguments of abc. The term constructed
by Agda is actually

> abc = \ {i} {A} -> id {i} {A} (id {i} {A -> A})

If you forbid Agda to introduce the implicit lambda abstractions (by
making all arguments explicit), it fails:

> id : (i : Level) (A : Set i) -> A -> A
> id i A x = x
>
> abc : (i : Level) (A : Set i) -> A -> A
> abc = id _ _ id
>
>> ((i : Level) (A : Set i) → A → A) !=< _11
>> because this would result in an invalid use of Setω
>> when checking that the expression id has type _11

The error means that you’re trying to apply a type constructor to
Setω, but that’s not allowed (as I said above, Setω is only allowed to
appear on its own and at the right-hand side of a typing judgment).

> is it then impossible to give id a
> type so that self application is possible, without yielding some form of
> inconsistency?

Well, you can do it using impredicativity.
For instance the following type-checks in Coq but gives a universe
inconsistency if you replace Prop by Type:

> Definition id (A : Prop) (x : A) : A := x.
> Check (id _ id).
>
>> id (forall A : Prop, A -> A) id
>>    : forall A : Prop, A -> A

But as far as I’m concerned, I don’t like impredicativity and I don’t
think I would want a type theory where you can apply id to itself,
that’s just too weird.

Guillaume