¿Qué es un super universo?

Estoy leyendo este conocido artículo sobre los universos en la teoría de tipos . Al principio esperaba algo similar a SetωAgda, pero resulta que es incluso algo más general. Parece generalizar la construcción del universo de un tipo simple inductivo-recursivo a una carpeta (similar a y Σ ). La pregunta principal que quiero hacer es, ¿cuál es la intención detrás de esto?$\Pi$$\Sigma$

Aquí hay un código Idris que define los universos habituales de estilo Tarski:

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

Estoy tratando de generalizarlo en algo como

mutual

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

¿Qué debería ???ser? El autor del artículo acaba de decir que los universos deberían cerrarse bajo formadores establecidos.

editar: creo que ???es simplemente b...

$U$

También hay un lado más práctico de tener muchos universos. Es útil tener tipos inductivos-recursivos en la teoría de tipos, para todo tipo de propósitos. Pero nos dejan definir nuevos universos, entonces la pregunta es ¿cuántos ? Para tener una idea de lo que está haciendo Palmgren, en lugar de disparar para el superuniverso de inmediato, intente la siguiente secuencia de construcciones en Agda (usando inducción-recursión):

1. $U_0$$\mathbb{N}$$\Pi$$\Sigma$

2. $U$$A$$A$$\Pi$$\Sigma$$U$$\mathbb{N}$

3. $V$

   • $V$$\mathbb{N}$$\Pi$$\Sigma$
   • $A : V$$B : A \to V$$U$$V$$B$$\Pi$$\Sigma$

   $V$$B : \mathbb{N} \to V$$B(n)$$n$$V$$U_\omega$