[Agda] More universe polymorphism

[Guillaume Brunerie]

Hi all,

Quick recall of Agda’s universe polymorphism:

There is a type Level of universe levels together with the following constants:

zero : Level
suc : Level -> Level
max : Level -> Level -> Level

For every i : Level, there is a universe Set i, which is also a term
of type Set (suc i).
A dependent product (x : A) -> B x such that A : Set i and B x : Set j
for all x : A is of type Set (max i j) (note that j cannot depend on
x, it has to be uniform).
Moreover, the type of universe levels Level is itself small (of type Type zero).


Why is Level required to be small?

If we drop this requirement, it seems to me that we could extend max
so that we can get the maximum of any small family of universe levels,
i.e. have some max2 of type:

max2 : (i : Level) (A : Set i) (j : A -> Level) -> Level

Then a dependent product (x : A) -> B x where A : Set i and B x : Set
(j x) would be of type Set (max2 i A j), so there is no "uniformity of
levels" restriction anymore, the only restriction is that the domain
and the codomain(s) are small.
You need the condition that Level is not small, or else you would be
able to define the max of all levels, which is likely to cause some
trouble.

Such universe polymorphism would permit to define a lot of new
universes, indexed by a lot of big countable ordinals (maybe up to the
Feferman–Schütte ordinal?)

Does that make sense? Is that consistent?
Did I miss something obvious?
I think there was something requiring Level to be small, but I don’t
remember what it is.

Guillaume