Что такое супер вселенная?

Я читаю эту известную статью о вселенных в теории типов . Сначала я ожидал чего-то подобного Setωв Агде, но оказалось, что это даже что-то более общее. Кажется, это обобщает построение вселенной от простого индуктивно-рекурсивного типа до связующего (аналогично и ). Главный вопрос, который я хочу задать, - что за этим стоит?$\Pi$$\Sigma$

Вот код Idris, определяющий обычные вселенные в стиле Тарского:

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

Я пытаюсь обобщить это в нечто вроде

mutual

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

Что должно ???быть? Автор статьи только что сказал, что вселенные должны быть закрыты в соответствии с установленными формами.

редактировать: я думаю, ???это просто b...

Одна из целей создания оператора вселенной и закрытой под ним супер-вселенной состоит в том, чтобы дать теоретико-типовую версию больших кардинальных аксиом, известных из теории множеств. Недостижимое кардинальное подобен вселенной типа теоретико-. Следующим интересным видом кардинала является кардинал Мало . Говоря интуитивно, кардинал Мало - это тот, у кого «много» недоступных кардиналов. Что бы это было в терминах теории типов? Это должна быть какая-то вселенная с множеством вселенных. Это то, к чему обращается Палмгрен, когда рассматривает супер-вселенные.$U$

Существует также более практическая сторона наличия множества вселенных. Полезно иметь индуктивно-рекурсивные типы в теории типов для любых целей. Но они позволяют нам определять новые вселенные, поэтому вопрос в том, сколько ? Чтобы понять, что делает Palmgren, вместо того, чтобы сразу же стрелять в супер-вселенную, попробуйте следующую последовательность конструкций в Agda (используя индукцию-рекурсию):

1. Определите одну вселенную , содержащую (код) N и замкнутую относительно Π и Σ . Этот вид вселенной соответствует недоступному кардиналу .$U_0$$\mathbb{N}$$\Pi$$\Sigma$

2. Определите оператор который принимает любой тип и определяет юниверс, который содержит (код) и замкнут относительно Π и Σ . Такого рода оператор вселенной сродни аксиоме вселенной Гротендика . Сколько вселенных мы можем получить, многократно применяя U , начиная с N ?$U$$A$$A$$\Pi$$\Sigma$$U$$\mathbb{N}$

3. Чтобы получить еще больше вселенных, мы постулируем супер-вселенную которая содержит множество вселенных, следующим образом:$V$

   • содержит N и замкнуто относительно Π и$V$$\mathbb{N}$$\Pi$$\Sigma$
   • Для данного (кода) типа и семейства B : A → V существует универсум U , который является элементом V , содержит все типы семейства B и замкнут относительно Π и Σ .$A : V$$B : A \to V$$U$$V$$B$$\Pi$$\Sigma$

   Сколько вселенных содержит ? Обратите внимание, что мы можем получить семейство B : N → V, такое, что B ( n ) - это n-я вселенная, и поэтому V должен содержать вселенную U ω, которая содержит все из них. И это только начало!$V$$B : \mathbb{N} \to V$$B(n)$$n$$V$$U_\omega$