O que é um super universo?

Estou lendo este artigo bem conhecido sobre Universos na teoria dos tipos . No começo, eu esperava algo semelhante ao Setωda Agda, mas acontece que é algo ainda mais geral. Parece generalizar a construção do universo de um tipo indutivo-recursivo simples para um aglutinante (semelhante a e ). A principal pergunta que quero fazer é: qual é a intenção por trás disso?$\Pi$$\Sigma$

Aqui estão alguns códigos Idris que definem os universos usuais no 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

Estou tentando generalizá-lo em algo como

mutual

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

O que deveria ???ser? O autor do artigo acabou de dizer que os universos devem ser fechados sob formadores.

edit: Eu acho que ???é simplesmente b...

Uma intenção por trás de ter um operador do universo e um super-universo fechado sob ele é fornecer uma versão teórica do tipo de grandes axiomas cardinais conhecidos da teoria dos conjuntos. Um cardeal inacessível é como um universo teórico do tipo. O próximo tipo interessante de cardeal é o cardeal Mahlo . Falando intuitivamente, um cardeal Mahlo é aquele que tem "muitos" cardeais inacessíveis abaixo dele. O que seria isso em termos teóricos do tipo? Deveria ser algum tipo de universo com muitos e muitos universos. É isso que Palmgren está abordando quando considera super-universos.$U$

Há também um lado mais prático em ter muitos universos. É útil ter tipos indutivo-recursivos na teoria dos tipos, para todos os tipos de propósitos. Mas eles nos permitem definir novos universos, então a questão é quantos ? Para ter uma ideia do que Palmgren está fazendo, em vez de fotografar o super-universo imediatamente, tente a seguinte sequência de construções no Agda (usando indução-recursão):

1. Defina um universo , contendo (um código de) e fechado em e . Esse tipo de universo corresponde a um cardeal inacessível .$U_0$$\mathbb{N}$$\Pi$$\Sigma$

2. Defina um operador que aceita qualquer tipo e define um universo que contém (um código de) e é fechado em e . Esse tipo de operador do universo é semelhante ao axioma de universos de Grothendieck . Quantos universos podemos obter aplicando repetidamente , começando em ?$U$$A$$A$$\Pi$$\Sigma$$U$$\mathbb{N}$

3. Para obter ainda mais universos, postulamos um super-universo que contém muitos universos, como segue:$V$

   • $V$ contém e está fechado em e$\mathbb{N}$$\Pi$$\Sigma$
   • Dado (código de) um tipo e uma família , existe um universo , que é um elemento de , contém todos os tipos da família e está fechado em e .$A : V$$B : A \to V$$U$$V$$B$$\Pi$$\Sigma$

   Quantos universos contém? Note que podemos obter uma família modo que seja o ésimo universo e, portanto, deve conter um universo que contenha todos esses . E este é apenas o começo!$V$$B : \mathbb{N} \to V$$B(n)$$n$$V$$U_\omega$