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

[Peter Hancock]

On 01/07/2013 19:58, Darryl McAdams wrote:
> Do levels really have to be things at all?

Well, I'm not sure what a thing is, but I think I agree with you,
if things are elements of sets.

> If we think of levels as
> merely/purely syntactic elements of the type theory, then it seems
> like the relational judgment "type_n" that Martin mentions would
> sidestep the issue entirely.

Aren't natural numbers things?  There's a set of them.  Natural
numbers aren't syntactical.

>Levels would no more exist in the model
> then ":" and "valid-context" do. - darryl

My favourite natural number (after zero) is 1.  It is impervious to arguments
about strick finitism, or general vertigo about the transfinite.

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?

Hank