Перейти к основному содержимому

HoTT как извлечение

Статус​

[Т-набр] — детали .

Обзор​

HoTT (Homotopy Type Theory) — современное альтернативное основание, предложенное Эводи, Воеводский, Coquand и другими (HoTT Book 2013). В Diakrisis: артикуляция α_HoTT ∈ ⟪⟫.

Значение HoTT​

  • Первое serious альтернативное основание к ZFC за десятилетия.
  • Univalent Foundations — программа Воеводского для пересмотра мат-оснований.
  • Computational meaning: HoTT допускает конструктивную интерпретацию.
  • Интеграция с гомотопической теорией: типы ≈ ∞-groupoids.

α_HoTT​

ν_{α_HoTT} = ω + 1 (параллельно α_ETCS, но другая ветвь Trace(𝖠)).

Почему ω+1​

  • Базовые типы — на уровне ω (аналогично ZFC).
  • Унивалентность добавляет «+1» — структура, не сводимая к обычной теории множеств.
  • α_HoTT и α_ETCS — одна ν, но разные gauge-классы.

Конструкция α_HoTT​

  • Ob(α_HoTT): типы.
  • Hom(A, B): функции A → B (в HoTT-смысле).
  • 2-морфизмы: гомотопии между функциями.
  • α_math: universe U_0 (type of small types).

В отличие от α_ZFC, α_HoTT естественно имеет 2-категорную структуру (через гомотопии), даже на «базовом» уровне.

Структурные инварианты​

  • Базовые типы.
  • Зависимые типы (Π, Σ).
  • Identity-типы.
  • Унивалентность (UA).
  • Higher inductive types.
  • Иерархия универсумов.

Детализация структурных инвариантов​

Базовые типы:

  • Empty type 0 (initial).
  • Unit type 1 (terminal).
  • Natural numbers ℕ.
  • Boolean 2.
  • и т.д.

Зависимые типы:

  • Π (A, B) — продукт зависимых типов (функциональные типы).
  • Σ (A, B) — сумма зависимых типов (сигма-типы).
  • В ⟪⟫: соответствуют product и coproduct adjoint парам.

Identity types:

  • Id_A(x, y) — тип «равенства» x = y в A.
  • В HoTT: Id — не тривиальный (может иметь нетривиальную структуру).
  • В ⟪⟫: соответствует диагонали Δ.

Унивалентность (UA):

  • Ключевая аксиома: (A = B) ≃ (A ≃ B).
  • Делает HoTT отличным от MLTT.
  • В Diakrisis: gauge-симметрия (см. ниже).

Higher inductive types (HIT):

  • Типы, определённые через конструкторы + path-конструкторы.
  • Примеры: circle S¹, sphere S², interval I.
  • В Diakrisis: специфические артикуляции с path-структурой.

Иерархия universes:

  • U_0 : U_1 : U_2 : ...
  • Каждый U_i — «тип типов» на уровне i.
  • В Diakrisis: иерархия 𝖬-итераций.

Ключевое соответствие​

03.T3: Унивалентность = gauge-инвариантность.

UA утверждает: (A ≃ B) ≃ (A = B). Изоморфизм = равенство.

В Diakrisis: это — принцип gauge-симметрии: Морита-эквивалентные артикуляции отождествляются. UA — конкретное воплощение.

Формализация соответствия​

  • В HoTT: функция ua: (A ≃ B) → (A = B) как аксиома.
  • В Diakrisis: для α, β ∈ ⟪⟫, если α ∼_gauge β, то [α] = [β] в 𝓜_Fnd.

Структурно: UA — конкретное выражение gauge-структуры для типов.

Философское значение​

Унивалентность отражает интуицию:

  • Структурно идентичные объекты должны быть математически одинаковы.
  • Не должно быть «скрытых отличий» между эквивалентными типами.

В Diakrisis: это — общий принцип gauge-симметрии, применённый к типам.

Cubical HoTT​

03.T5: α_cubical = 𝖬(α_HoTT) (с вычислительной структурой).

Cubical Type Theory​

  • Введена Cohen-Coquand-Huber-Mörtberg (2015).
  • Даёт вычислительную интерпретацию univalence.
  • Основана на cubical sets (вместо simplicial).

Соответствие в Diakrisis​

  • α_HoTT — «не-вычислительный» вариант.
  • α_cubical = 𝖬(α_HoTT) — «вычислительный» (через метаизацию).
  • В ⟪⟫: α_cubical ⊏_1 α_HoTT.

Это — пример связи внутри одного gauge-класса через 𝖬-итерацию.

Kan complexes — модель​

03.T6: Kan-complexes — стандартная модель HoTT; соответствует α_math = α_simp_set.

Kan complexes​

  • Симплициальные множества, удовлетворяющие Kan condition.
  • Стандартная модель для ∞-groupoids.
  • Основа для гомотопической теории Quillen (1967).

Соответствие​

  • α_math = α_simp_set в случае HoTT.
  • ρ(α_HoTT) в этой модели — функтор на Kan complexes.
  • HoTT-типы ↔ Kan complexes.

∞-topos как контекст​

03.T7: HoTT — внутренний язык ∞-топосов. α_HoTT ⊏κ α∞topos.

Внутренний язык​

  • Внутренний язык категории C — это язык, в котором утверждения о C выражаются внутри C.
  • HoTT — внутренний язык (∞,1)-топоса.
  • Каждый (∞,1)-топос даёт модель HoTT.

Связь в 𝓜_Fnd​

  • α_HoTT ⊏1 α∞topos (HoTT — частная форма ∞-topos).
  • Обратное: не каждый ∞-topos — HoTT (HoTT = ∞-topos с унивалентный universes).

Типы = ∞-groupoids​

03.C3: «типы — ∞-groupoids» — АПЕЙРОН-факт через 03.T6.

Формализация​

  • Тип A в HoTT.
  • A как ∞-groupoid: объекты = элементы A, морфизмы = paths, высшие морфизмы = paths of paths, и т.д.
  • Это — структурная интерпретация, не просто переименование.

Значение​

  • HoTT — первое основание, где «типы = ∞-groupoids» становится формальной тождественностью.
  • Интеграция с гомотопической теорией — естественна, не вынужденна.

Морита с другими​

  • α_MLTT ∼_{gauge} α_HoTT (с UA).
  • α_Univalent-Fnd ∼_{gauge} α_HoTT.

Детализация​

MLTT + UA ∼ HoTT:

  • MLTT (Мартин-Лёф Type Theory) + Унивалентность Axiom = HoTT.
  • Без UA: MLTT — другой gauge-класс.

Univalent Foundations:

  • Проект Воеводского.
  • Ближайший конкретный практический вариант HoTT.
  • Морита-эквивалентен α_HoTT.

Какие основания не Морита-эквивалентны α_HoTT​

  • ZFC/ETCS: разные gauge-классы (UA отсутствует).
  • NCG: разные gauge-классы (другая специфика).
  • УГМ: ν_uhm = ω·3+1 vs ν_HoTT = ω+1.

Признанные редукции​

  • Стандартная HoTT-теория.
  • Унивалентность = (относительно известно).
  • ∞-topos контекст — Люри.

Источники​

  • Эводи-Уоррен (2009): Homotopy теория типов.
  • Воеводский (2010+): Univalent Foundations program.
  • HoTT Book (2013): каноническая формализация.
  • Шульман (2015+): теоретические results.
  • Coquand et al. (2015): Cubical теория типов.
  • Люри (2009): HTT — ∞-topos context.

Специфика извлечения HoTT​

Конструктивность​

  • HoTT поддерживает конструктивную интерпретацию (особенно cubical).
  • В Diakrisis: α_HoTT имеет дополнительную computational structure.

Путь к Verum​

  • HoTT — одна из наиболее разработанных формализаций в современных proof-assistants.
  • Agda, Coq (с HoTT-library), Lean 4 (с mathlib HoTT) — поддерживают.
  • Verum для УГМ должен учитывать HoTT-подход.

Открытые вопросы​

  • Каноническая модель cubical: варианты.
  • Higher inductive types: классификация.
  • Относительность к ZFC: Воеводский показал консистентность HoTT в ZFC.

Применение HoTT в Diakrisis​

Как источник gauge-интуиции​

UA в HoTT даёт явный принцип gauge-симметрии. Это вдохновляет наш подход к gauge-структуре ⟪⟫.

Как кандидат формализации​

  • Diakrisis частично может быть формализован в HoTT.
  • 2-категорная структура ⟪⟫ — через типы-как-∞-groupoids.
  • Унивалентность — через gauge.

Ограничения​

  • HoTT — уровень 5 (как и ZFC).
  • Не может выразить AFN-T (мета-утверждение).
  • Diakrisis не сводим к HoTT (хотя использует похожие идеи).

Следующий документ​

/04-extractions/03-ncg.