Гомотопическая теория типов

Владимир Воеводский в 2009 году сформулировал аксиому унивалентности, доказав её непротиворечивость через симплициальную семантику. В 2013 году Институт перспективных исследований опубликовал «Homotopy Type Theory» - книгу, написанную коллаборацией из 50 математиков за год.

• Формальная математика: Lean 4, Agda, Coq - системы формальных доказательств на основе зависимых типов
• Кубическая вычислительная семантика: Agda с кубическим расширением проверяет теоремы HoTT компьютером
• ∞-категории: HoTT - синтетическая теория ∞-группоидов, аналог Луи-теории без модельных категорий

Предварительные знания

• Предыдущий урок

Типы как ∞-группоиды

Гомотопическая теория типов выросла из аксиомы унивалентности Воеводского (2006) и оформилась в книге HoTT Book, написанной программой Univalent Foundations в IAS в 2013 году. Формализации в Coq и Lean проверяют доказательства объёмом в тысячи страниц, а реализация кубической теории типов cubicaltt (2016) напрямую вычисляет аксиому унивалентности.

В HoTT каждый тип A имеет h-уровень. A контрактилен (h-уровень −2), если ∃ a₀: ∀ a, a = a₀. A - предложение (h-уровень −1), если ∀ a b: A, a = b. A - множество (h-уровень 0), если все пути a = b контрактильны. Тип h-уровня n+1: все Id_A(a,b) имеют h-уровень ≤ n. Аксиома унивалентности: (A = B) ≃ (A ≃ B).

Высшие индуктивные типы

Высший индуктивный тип (HIT) задаётся точечными и путевыми конструкторами. S¹ = {base : S¹; loop : base = base}. Кольцо Z строится как S¹-cover. n-усечение ||A||_n: добавляет конструктор, делающий h-уровень ≤ n. Суспензия ΣA, джойн A * B - HITs. Кубическая теория типов делает унивалентность и HITs вычислимыми.

Ключевые идеи

• Типы - ∞-группоиды: h-уровень(A) измеряет «сложность» пространства путей
• Унивалентность: (A = B) ≃ (A ≃ B) - изоморфные типы тождественны
• π₁(S¹) = Z: доказано в HoTT через encode-decode без топологии
• HIT: S¹ = {base, loop}, суспензия, усечение - алгебраические конструкции
• Кубическая TTT: унивалентность вычислима, HITs имеют определённую семантику

Дальнейшие пути

Изученные концепции открывают следующие разделы.

• ct-28-model-categories — extends

Вопросы для размышления

• Приведите конкретный пример вычисления.
• Как изученные концепции связаны с другими разделами математики?

Связанные уроки

• qc-01
• qc-02