[Agda] Formalization of Agda's universe polymorphism

[Roman]

"On Universes in Type Theory", Erik Palmgren [1] -- is one related
paper. It describes a Tarski-style tower of universes and then adds a
super universe to this tower.

Agda has a Russell-style tower of noncumulative universes. As the paper states:

    The Russell formulation should be regarded as an informal version
of the Tarski formulation

Agda also has a super universe, because `∀ α -> Set α` is a legal type
in Agda (but not a legal term), but that super universe is only closed
over `∀` since `∃ λ α -> Set α` is rejected.

I translated a part of the paper to Agda: [2] (universes are
cumulative). This should be easier to read, but take it with a grain
of salt.

[1] http://www2.math.uu.se/~palmgren/universe.pdf
[2] https://github.com/effectfully/random-stuff/blob/master/Omega.agda