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

[Peter Hancock]

On 01/07/2013 17:04, Martin Escardo wrote:
> Ok, I understand, Guillaume. The crucial thing, in your formulation
> below of transfinite universes, is that Level is a type but cannot
> live in a universe, right? (So it doesn't have a type.)

In set theory, ordinals (that index the cumuluative hierarchy)
form a class, just like sets.   So, they don't live in any universe,
at least not in the sense of a Grothendieck universe.  They are
"commensurate" with the notion of set itself.

The notion of "set" (or whatever you want to call it)
is inexpressible in Agda. That is why Martin-Lof (and G. Brunerie)
proposes a judgement form for it different from a : A.  If Agda
had the notion of set, by the same token, it would have a coherent
notion of level.

One hundred years ago, we had Principia mathematica, which was a
ramified theory, with "levels" (short circuited by reducibility,
but never mind).  Nobody knew what type they lived in, or what the
level of that type should be.  It seems to me that in 100 years,
we have travelled precisely nowhere.

Hank