[Agda] universe levels

[Martin Escardo]

For most purposes, Set0, Set1, Set2, Set3, suffice (has anybody got
higher than that?). However, for the sake of uniformity, it is useful
to have a countable sequence of type universes Set i, which Agda
thankfully has. Now, if you want to formalize a type theory having
countably many such universes Set i, in Agda, you find that you need
a further universe Set omega.

(You could instead try to formalize a type theory with n universes using
a type theory with n+1 universes. I tried that, and it becomes
cumbersome. We need n-many definitions of things that look the same
(the type Fin n doesn't help, because n (being a natural number)
cannot depend on a level, as levels cannot be eliminated (which is
sensible if one is trying to avoid inconsistency)).

However, it is not clean (or uniform) to extend Agda with a limit type
universe Set omega.

A cleaner solution, I think, would be to add a Level constructor

  sup : (Nat -> Level) -> Level.

Of course, we are talking about ordinals, but not first-class-citizen
ordinals, only ordinal levels (that can be created, but not eliminated
- which is important to avoid Paradox Land).

Whatever is obtained in this direction, should be (by design)
relatively easy to implement as part of the Agda type checker.
(Agda implementors: is it easy to add sup as Level constructor?
(Ignoring logical issues of consistency, which can be left to all of us
to think about independently of the implementation.))

Anyway, I was trying to write some Agda definitions just now, which
look good to me, but unfortunately I will have to tell agda to accept
a potential inconsistency by enabling type-in-type (and removing all my
neat universe level decorations, which don't harmonize with
type-in-type, but would if we had universe levels as above).


Martin