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

[Darryl McAdams]

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