What is a super universe?

I'm reading this well-known paper On Universes in Type Theory.
At first I expected something similar to Setω in Agda, but it turns out that it's even something more general.
It seems to generalize the universe construction from a plain inductive-recursive type to a binder (similar to $\Pi$ and $\Sigma$).
The main question I want to ask is, what's the intention behind it?

Here's some Idris code defining usual Tarski-style universes:

mutual

  public export data U : (level : Nat) -> Type where
    GroundU : Ground -> U level
    BinderU : Binder -> (a : U level) -> (b : (x : T {level} a) -> U level) -> U level
    UnivU   : U (S level)
    LiftU   : U level -> U (S level)

  public export T : {level : Nat} -> (code : U level) -> Type

I'm trying to generalize it into something like

mutual

  public export data U : (a : Type) -> (b : (x : a) -> Type) -> Type where
    GroundU : Ground -> U a ???
    ...

What should ??? be? The author of the paper just said universes should be closed under set formers.

edit: I think ??? is simply b ...

One intention behind having a universe operator and a super-universe closed under it, is to give a type-theoretic version of large cardinal axioms known from set theory. An inaccessible cardinal is like a type-theoretic universe. The next interesting kind of cardinal is a Mahlo cardinal. Speaking intuitively, a Mahlo cardinal is one that has "a whole lot" of inaccessible cardinals below it. What would this be in type-theoretic terms? It ought to be some sort of a universe $U$ with lots and lots of universes in it. This is what Palmgren is addressing when he considers super-universes.

There is also a more practical side to having many universes. It is useful to have inductive-recursive types in type theory, for all sorts of purposes. But they let us define new universes, so the question is how many? To get a feel for what Palmgren is doing, instead of shooting for the super-universe right away, try the following sequence of constructions in Agda (using induction-recursion):

-
Define one universe $U_0$, containing (a code of) $\mathbb{N}$ and closed under $\Pi$ and $\Sigma$. This kind of universe corresponds to an inaccessible cardinal.

-
Define an operator $U$ which takes any type $A$ and defines a universe which contains (a code of) $A$ and is closed under $\Pi$ and $\Sigma$. This sort of universe operator is akin to Grothendieck's axiom of universes. How many universes can we get by repeatedly applying $U$, starting from $\mathbb{N}$?

-
To get even more universes, we postulate a super-universe $V$ which contains lots of universes, as follows:

• $V$ contains $\mathbb{N}$, and is closed under $\Pi$ and $\Sigma$

• Given (code of) a type $A : V$ and a family $B : A \to V$, there is a universe $U$, which is an element of $V$, it contains all types of the family $B$, and is closed under $\Pi$ and $\Sigma$.

How many universes does $V$ contain? Note that we can get a family $B : \mathbb{N} \to V$ such that $B(n)$ is the $n$-th universe, and so $V$ must contain a universe $U_\omega$ which contains all of these. And this is only the beginning!

StackExchange Computer Science Q#68014, answer score: 11