Was ist ein Superuniversum?

Ich lese diesen bekannten Artikel über Universen in der Typentheorie . Zuerst habe ich etwas Ähnliches wie Setωin Agda erwartet , aber es stellt sich heraus, dass es noch etwas allgemeineres ist. Es scheint die Universumskonstruktion von einem einfachen induktiv-rekursiven Typ auf ein Bindemittel (ähnlich wie und Σ ) zu verallgemeinern . Die Hauptfrage, die ich stellen möchte, ist, was ist die Absicht dahinter?$\Pi$$\Sigma$

Hier ist ein Idris-Code, der übliche Universen im Tarski-Stil definiert:

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

Ich versuche es in so etwas zu verallgemeinern

mutual

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

Was soll ???sein Der Autor des Papiers sagte gerade, Universen sollten unter festgelegten Formern geschlossen werden.

edit: ich denke ???ist einfach b...

$U$

Viele Universen haben auch eine praktischere Seite. Es ist nützlich, induktiv-rekursive Typen in der Typentheorie für alle möglichen Zwecke zu haben. Aber sie lassen uns neue Universen definieren, also ist die Frage, wie viele ? Um ein Gefühl dafür zu bekommen, was Palmgren tut, versuchen Sie die folgende Abfolge von Konstruktionen in Agda (mithilfe der Induktionsrekursion), anstatt sofort nach dem Superuniversum zu schießen:

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$