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

[Guillaume Brunerie]

On 2013/7/1 Peter Hancock <hancock at spamcop.net> wrote:
> Why don't we just have one universe of Sets, memebership of which we express
> by a judgement, that is not a Set-inhabitation judgement, perhaps
> "A is a Set"?  Then among the sets, we can have universes like
> Gothendieck's, and index them by whatever mathematical things we like?

Is this universe of Sets supposed to be a term (then what’s its type?)
or a type (then what’s the difference between "A is a Set" and "A :
Set") or nothing?

I guess it’s neither a term nor a type, but then the judgment "A is a
Set" is what I call "A  type" and the question is how to index the
universes among the sets.


Guillaume