HoTT
Первая половина 2019-го оказалась урожайна на результаты касательно семантики Гомотопической Теории Типов.
Результаты касаются так называемой Book HoTT, т.е. варианта гомотопической теории типов, описанного в одноимённой книжке. Однако, в когда была написана книжка, ещё не было понимания, что же такое высшие индуктивные типы в общем виде. Поэтому на практике это три версии, параметризованные ординалом n от 0 до ω:
- HoTTMin(n) это гомотопическая теория типов с иерархией из n унивалентных вселенных, содержащими типы 0, 1, 2, Nat и замкнутыми относительно формирования всевозможных Σ, Π и Id типов.
- В HoTTMax(n) вселенным требуется дополнительно быть замкнутым относительно формирования всевозможных высших индуктивно-индуктивных типов, как они описываются в статье Ambrus Kaposi, András Kovács, «A Syntax for Higher Inductive-Inductive Types» - это очень обширный класс, включающий кроме всего прочего вещественные числа и синтаксические модели всевозможных обобщённых алгебраические теорий без равенств на сортах.
- В HoTTMid(n) требуется замкнутость не относительно всех высших индуктивных типов, но по меньшей мере W-типов, усечений, локализаций, пушаутов и рекурсивных клеточных комплексов.
Ну и у каждой из них есть вариант HoTTI с универсальным (импредикативным) типом утверждений.
Для конструирования моделей используется теория множеств, точнее два семейства теорий множеств:
- ZFC(n) стандартная теория множеств с аксиомой выбора + аксиомами о существовании n недостижимых кардиналов. Для конечных n ZFC(n + 1) доказывает непротиворечивость ZFC(n).
- CZF(n) конструктивная теория множеств с аксиомой о существовании n недостижимых транзитивных множеств. Тут тоже CZF(n + 1) доказывает непротиворечивость CZF(n), кроме того CZF(n) + исключённое третье + аксиома выбора = ZFC(n).
Теперь можно о результатах. Во-первых, Шульман получил могучий результат, что HoTTMid таки моделируется в любом гротендиковом ∞-топосе: ZFC(n) доказывает, что любой гротендиков ∞-топос может быть представлен модельной категорией, реализующей интерпретацию HoTTMid, I(n).
Во-вторых, по модулю некоторых (по утверждению специалистов, решаемых) вопросов высшей когерентности реализована конструктивная симплициальная модель HoTT. https://arxiv.org/abs/1905.06281, там показывают что CZF(1) позволяет собрать (ну, почти) модель HoTTMin(1).
Во-третьих, Christian Sattler и Krzysztof Kapulkin анонсировали доказательство гипотезы Воеводского о гомотопической каноничности HoTT (мне пока точно неизвестно в какой из версий).
Очень жаль, что Воеводский не дожил.
Результаты касаются так называемой Book HoTT, т.е. варианта гомотопической теории типов, описанного в одноимённой книжке. Однако, в когда была написана книжка, ещё не было понимания, что же такое высшие индуктивные типы в общем виде. Поэтому на практике это три версии, параметризованные ординалом n от 0 до ω:
- HoTTMin(n) это гомотопическая теория типов с иерархией из n унивалентных вселенных, содержащими типы 0, 1, 2, Nat и замкнутыми относительно формирования всевозможных Σ, Π и Id типов.
- В HoTTMax(n) вселенным требуется дополнительно быть замкнутым относительно формирования всевозможных высших индуктивно-индуктивных типов, как они описываются в статье Ambrus Kaposi, András Kovács, «A Syntax for Higher Inductive-Inductive Types» - это очень обширный класс, включающий кроме всего прочего вещественные числа и синтаксические модели всевозможных обобщённых алгебраические теорий без равенств на сортах.
- В HoTTMid(n) требуется замкнутость не относительно всех высших индуктивных типов, но по меньшей мере W-типов, усечений, локализаций, пушаутов и рекурсивных клеточных комплексов.
Ну и у каждой из них есть вариант HoTTI с универсальным (импредикативным) типом утверждений.
Для конструирования моделей используется теория множеств, точнее два семейства теорий множеств:
- ZFC(n) стандартная теория множеств с аксиомой выбора + аксиомами о существовании n недостижимых кардиналов. Для конечных n ZFC(n + 1) доказывает непротиворечивость ZFC(n).
- CZF(n) конструктивная теория множеств с аксиомой о существовании n недостижимых транзитивных множеств. Тут тоже CZF(n + 1) доказывает непротиворечивость CZF(n), кроме того CZF(n) + исключённое третье + аксиома выбора = ZFC(n).
Теперь можно о результатах. Во-первых, Шульман получил могучий результат, что HoTTMid таки моделируется в любом гротендиковом ∞-топосе: ZFC(n) доказывает, что любой гротендиков ∞-топос может быть представлен модельной категорией, реализующей интерпретацию HoTTMid, I(n).
Во-вторых, по модулю некоторых (по утверждению специалистов, решаемых) вопросов высшей когерентности реализована конструктивная симплициальная модель HoTT. https://arxiv.org/abs/1905.06281, там показывают что CZF(1) позволяет собрать (ну, почти) модель HoTTMin(1).
Во-третьих, Christian Sattler и Krzysztof Kapulkin анонсировали доказательство гипотезы Воеводского о гомотопической каноничности HoTT (мне пока точно неизвестно в какой из версий).
Очень жаль, что Воеводский не дожил.