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

[Darryl McAdams]

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

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. is it then impossible to give id a type so that self application is possible, without yielding some form of inconsistency?
 
- darryl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130630/04b6a079/attachment-0001.html