Co to jest super wszechświat?

Czytam ten dobrze znany artykuł o wszechświatach w teorii typów . Na początku spodziewałem się czegoś podobnego do SetωAgdy, ale okazuje się, że jest to nawet coś bardziej ogólnego. Wydaje się uogólniać konstrukcję wszechświata od zwykłego typu indukcyjno-rekurencyjnego do spoiwa (podobnego do$\Pi$ i $\Sigma$). Główne pytanie, które chcę zadać, to jaki jest tego zamiar?

Oto kod Idris definiujący zwykłe wszechświaty w stylu Tarskiego:

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

Próbuję uogólnić na coś takiego

mutual

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

Co powinno ???być Autor artykułu powiedział właśnie, że wszechświaty powinny być zamknięte pod ustalonymi twórcami.

edycja: Myślę, że ???jest po prostu b...

Jednym z celów stojących za zamkniętym pod nim operatorem wszechświata i superwszechświatem jest podanie teoretycznej wersji dużych kardynalnych aksjomatów znanych z teorii mnogości. Liczba nieosiągalna jest jak typ-teoretyczny wszechświata. Kolejnym interesującym rodzajem kardynała jest kardynał Mahlo . Mówiąc intuicyjnie, kardynał Mahlo to taki, który ma pod sobą „całą masę” niedostępnych kardynałów. Co by to było w kategoriach teoretycznych? To powinien być jakiś wszechświat$U$z dużą ilością wszechświatów. Do tego zmierza Palmgren, gdy rozważa superwszechświaty.

Istnieje również bardziej praktyczna strona posiadania wielu wszechświatów. Przydatne jest posiadanie typów indukcyjno-rekurencyjnych w teorii typów do różnych celów. Ale pozwalają nam zdefiniować nowe wszechświaty, więc pytanie brzmi: ile ? Aby poczuć, co robi Palmgren, zamiast od razu strzelać do superwszechświata, wypróbuj następującą sekwencję konstrukcji w Agda (używając rekurencji-indukcji):

1. Zdefiniuj jeden wszechświat $U_0$, zawierający (kod) $\mathbb{N}$ i zamknięty pod $\Pi$ i $\Sigma$. Ten rodzaj wszechświata odpowiada niedostępnemu kardynałowi .

2. Zdefiniuj operatora $U$ który przyjmuje dowolny typ $A$ i definiuje wszechświat, który zawiera (kod) $A$ i jest zamknięty pod $\Pi$ i $\Sigma$. Ten rodzaj operatora wszechświata jest podobny do aksjomatu wszechświatów Grothendiecka . Ile wszechświatów możemy uzyskać poprzez wielokrotne stosowanie$U$, zaczynając od $\mathbb{N}$?

3. Aby uzyskać jeszcze więcej wszechświatów, postulujemy superwszechświat $V$ który zawiera wiele wszechświatów, jak następuje:

   • $V$ zawiera $\mathbb{N}$i jest zamknięty pod $\Pi$ i $\Sigma$
   • Podany (kod) typ $A : V$ i rodzina $B : A \to V$istnieje wszechświat $U$, który jest elementem $V$, zawiera wszystkie typy rodziny $B$i jest zamknięty pod $\Pi$ i $\Sigma$.

   Ile wszechświatów robi $V$zawierać? Pamiętaj, że możemy dostać rodzinę$B : \mathbb{N} \to V$ takie, że $B(n)$ jest $n$-ty wszechświat i tak dalej $V$ musi zawierać wszechświat $U_\omega$który zawiera je wszystkie. A to dopiero początek!