Гомотопическая теория типов (HoTT, от англ. homotopy type theory) — математическая теория, особый вариант теории типов, снабжённый понятиями из теории категорий, алгебраической топологии, гомологической алгебры; базируется на взаимосвязи между понятиями о гомотопическом типе пространства, высших категориях^[англ.] и типах в логике и языках программирования.

Унивалентные основания математики — программа построения средствами гомотопической теории типов универсального формального языка, являющегося конструктивными основаниями для современных разделов математики и обеспечивающего возможность автоматической проверки правильности доказательств на компьютере. Инициирована Владимиром Воеводским в конце 2000-х годов; толчком к более широкому интересу к унивалентным основаниям послужила написанная Воеводским библиотека формализованной математики «Foundations», ставшая к середине 2010-х годов частью библиотеки UniMath и послужившая основой для многих других библиотек➤; в рамках программы большим коллективом математиков была написана книга➤.

Математическое доказательство в гомотопической теории типов состоит в установлении «обитаемости» необходимого типа, то есть, в построении выражения соответствующего типа. Использование систем автоматического доказательства для теории эксплуатирует идею изоморфизма Карри — Ховарда, а благодаря математическому содержанию, вложенному в теоретико-типовые понятия, на формальном языке теории удаётся выразить и проверить достаточно сложные результаты из абстрактных разделов математики, которые ранее считались не формализуемыми программными средствами.

Ключевая идея теории — аксиома унивалентности➤, постулирующая равенство объектов, между которыми может быть установлена эквивалентность, то есть, в гомотопической теории типов как равные рассматриваются изоморфные, гомеоморфные, гомотопически эквивалентные структуры; эта аксиома отражает важные свойства интерпретации высшей категории, а также обеспечивает техническое упрощение формального языка.

Идея использования интуиционистской теории типов Пера Мартин-Лёфа для формализации высших категорий восходит к работе Михая Маккаи (венг. Makkai Mihály), в которой была построена система FOLDS (англ. first-order logic with dependent sorts)^[1]. Ключевым отличием унивалентных оснований от идей Маккаи является принцип, согласно которому фундаментальными объектами математики являются не высшие категории, а высшие группоиды. Поскольку высшие группоиды отвечают по соответствию Гротендика гомотопическим типам, можно сказать, что математика, с точки зрения унивалентных оснований, изучает структуры на гомотопических типах. Возможность прямого использования теории типов Мартин-Лёфа для описания структур на гомотопических типах является следствием построения Воеводским унивалентной модели теории типов. Построение этой модели требовало решения многочисленных технических проблем связанных с так называемыми свойствами когерентности и, хотя основные идеи унивалентных оснований были сформулированны им в 2005—2006 годы, полная унивалентная модель в категории симплициальных множеств появилась только в 2009 году. В те же годы, что и эти исследования Воеводского, велись и другие работы по изучению различных связей между теорией типов и теорией гомотопий, в частности, одним из исторически важных событий, собравшим учёных, работавших в этом направлении, стал семинар в Уппсале в ноябре 2006 года^[2].

В феврале 2010 года Воеводский начал создавать библиотеку на Coq, выросшую впоследствии в совместно разрабатываемую широким кругом учёных «библиотеку унивалентных оснований»➤.

По инициативе Воеводского, 2012—2013 академический год в Институте перспективных исследований был объявлен «годом унивалентных оснований», в сотрудничестве с Ауди и Коканом была открыта специальная исследовательская программа и в её рамках группа из математиков и специалистов по информатике работали над развитием теории. Одним из результатов года стало совместное создание участниками шестисотстраничной книги «Гомотопическая теория типов: унивалентные основания математики», выложенной на сайте программы в свободный доступ под лицензией CC-SA; для совместной работы над книгой был создан проект на GitHub^[3].

Участники программы, представленные во введении к книге^[4]:

Кроме того, во введении указано, что значительный вклад внесли также шестеро студентов, а также отмечен вклад более 20-ти учёных и практиков, посетивших в течение «года унивалентых оснований» Институт высших исследований (среди которых создатель семантики λ-исчисления Дана Скотт и разработчик формализаций на Coq доказательств задачи о четырёх красках и теоремы Фейта — Томпсона Жорж Гонтье^[фр.]). Книга построена из двух частей — «Основания» и «Математика», в первой части излагаются основные положения и определяется инструментарий, во второй — строятся реализации введёнными средствами теории гомотопий, теории категорий, теории множеств, вещественных чисел.

Теория основывается на интенсиональном варианте интуиционистской теории типов Мартин-Лёфа и использует интерпретацию типов как объектов теории гомотопий и высших категорий. Так, с этой точки зрения отношение принадлежности точки пространству ${\displaystyle a\in A}$ рассматривается как терм соответствующего типа: ${\displaystyle a:A}$, расслоение с базой ${\displaystyle X}$ — как зависимый тип ${\displaystyle A(x)}$. При этом отпадает необходимость представлять пространства в виде множеств точек, снабжённых топологией, и представлять непрерывные отображения между пространствами — как функции сохраняющие или отражающие соответствующие поточечные свойства пространств. Гомотопическая теория типов рассматривает пространства-типы и термы этих типов (точки) как элементарные понятия, а конструкции над пространствами, такие как гомотопии и расслоения, — как зависимые типы.

В формальном построении теории типов используется тип-универсум ${\displaystyle {\mathcal {U}}_{0}}$, термы которого — все прочие неуниверсальные («малые») типы, далее строятся типы ${\displaystyle {\mathcal {U}}_{1},{\mathcal {U}}_{2},\dots }$ такие, что ${\displaystyle U_{i}:U_{i+1}}$, притом все термы типа ${\displaystyle {\mathcal {U}}_{i}}$ также являются термами типа ${\displaystyle {\mathcal {U}}_{i+1}}$. Зависимые типы (семейства типов) определяются как функции ${\displaystyle B:A\to {\mathcal {U}}}$, кообласть которых — некоторый тип-универсум.

В гомотопической теории типов существует несколько способов конструирования новых типов из уже имеющихся. Базовые примеры такого рода — ${\displaystyle {\boldsymbol {\Pi }}}$-типы (зависимые функциональные типы, типы-произведения) и ${\displaystyle {\boldsymbol {\Sigma }}}$-типы (зависимые типы-суммы). Для данного типа ${\displaystyle A:{\mathcal {U}}}$ и семейства ${\displaystyle B:A\to {\mathcal {U}}}$ можно построить тип ${\displaystyle {\boldsymbol {\Pi }}_{x:A}B(x)}$, термы которого — функции, кообласть которых зависит от элемента области определения (геометрически такие функции можно представлять как сечения некоторого расслоения), а также тип ${\displaystyle {\boldsymbol {\Sigma }}_{x:A}B(x)}$, термы которого геометрически соответствуют элементам тотального пространства расслоения.

Равенство термов одного и того же типа в гомотопической теории типов может быть либо равенством «по определению» (${\displaystyle a_{1}:=a_{2}}$), либо пропозициональным равенством. Равенство по определению влечёт пропозициональное равенство, но не наоборот. В общем случае, пропозициональное равенство термов ${\displaystyle a_{1}}$ и ${\displaystyle a_{2}}$ типа ${\displaystyle A}$ представляется в виде непустого типа ${\displaystyle {\mathsf {Id}}_{A}(a_{1},a_{2})}$, который называют типом тождества; термы этого последнего типа — это пути вида ${\displaystyle p:a_{1}\rightsquigarrow a_{2}}$ в пространстве ${\displaystyle A}$; тип тождества ${\displaystyle {\mathsf {Id}}_{A}(a_{1},a_{2})}$, таким образом, рассматривается как пространство путей (то есть непрерывных отображений единичного отрезка ${\displaystyle \mathbb {I} }$ в ${\displaystyle A}$) из точки ${\displaystyle a_{1}}$ в точку ${\displaystyle a_{2}}$.

Интуиционистская теория типов позволяет определить понятие эквивалентности типов (для типов принадлежащих одному универсуму) и построить каноническим образом функцию из типа тождества ${\displaystyle A=B}$ в тип эквивалентности ${\displaystyle A\simeq B}$:

${\displaystyle (A=B)\to (A\simeq B)}$.

Аксиома унивалентности, сформулированная Воеводским, утверждает, что эта функция также является эквивалентностью:

${\displaystyle (A=B)\simeq (A\simeq B)}$,

то есть, тип тождества двух данных типов эквивалентен типу эквивалентности этих типов. В случае если ${\displaystyle A}$ и ${\displaystyle B}$ — пропозициональные типы, аксиома имеет особенно прозрачный смысл и сводится к утверждению, который иногда называют принципом экстенсиональности Чёрча: равенство высказываний логически эквивалентно их логической эквивалентности; использование этого принципа означает, что во внимание принимаются только истинностные значения высказываний, но не их смысл. Следствием аксиомы является функциональная экстенсиональность^[англ.], то есть утверждение о том, что функции, значения которых равны для всех равных значений их аргументов, равны между собой. Это свойство функций имеет важное значение в информатике.

Аксиома рассматривается некоторыми философами математики в качестве точной математической формулировки основного тезиса философии математического структурализма^[англ.], которая опирается на распространённую практику математических рассуждений «с точностью до изоморфизма» или «с точностью до эквивалентности»^[5].

Высказывание (mere proposition, «голое высказывание») в гомотопической теории типов определяется как тип ${\displaystyle P}$, который либо пуст, либо содержит единственный терм ${\displaystyle p}$; такие типы называются пропозициональными. Если тип ${\displaystyle P}$ пуст, то соответствующее высказывание ложно, если ${\displaystyle P}$ содержит терм ${\displaystyle p}$ (символически — ${\displaystyle p:P}$), то соответствующее высказывание ${\displaystyle P}$ истинно, а терм ${\displaystyle p}$ рассматривается как его доказательство. Таким образом, в теории используется интуиционистская концепция истины, согласно которой истинность высказывания понимается как возможность предъявить доказательство этого высказывания.

Фрагмент гомотопической теории типов, который ограничивается операциями с пропозициональными типами, то есть с высказываниями, можно описать как логический фрагмент (логику) этой теории. Логическая дизъюнкция ${\displaystyle A\vee B}$ соответствует в пропозициональном фрагменте типу-сумме ${\displaystyle A+B}$, конъюнкция ${\displaystyle A\wedge B}$ — типу-произведению ${\displaystyle A\times B}$, импликация ${\displaystyle A\Rightarrow B}$ — функциональному типу ${\displaystyle A\to B}$, отрицание ${\displaystyle \lnot A}$ — типу ${\displaystyle A\to \mathbf {0} }$, где ${\displaystyle \mathbf {0} }$ — это пустой тип (нуль-тип). Логика, соответствующая таким конструкциям, является вариантом интуиционистской логики, в частности, в ней не имеют места такие утверждения, как закон двойного отрицания или исключённого третьего.

Всякий тип ${\displaystyle X}$, который содержит два или больше различных термов ${\displaystyle x,y,\dots }$ может быть поставлен в однозначное соответствие с пропозициональным типом, который получается в результате отождествления всех термов типа ${\displaystyle X}$, такая операция называется пропозициональным обрезанием (propositional truncation). Это позволяет провести различие между «пропозициональным уровнем» (уровнем высказываний) теории и гомотопической иерархии «высших» непропозициональных её уровней.

За уровнем высказываний следует уровень множеств. Множество в гомотопической теории типов определяется как пространство (тип) с дискретной топологией. Эквивалентно, множество ${\displaystyle A}$ можно описать в теории как тип, такой что для любых его термов ${\displaystyle a_{1},a_{2}:A}$ тип ${\displaystyle {\mathsf {Id}}_{A}(a_{1},a_{2})}$ является высказыванием, то есть либо пуст (случай когда ${\displaystyle a_{1}}$ и ${\displaystyle a_{2}}$ — это различные элементы множества ${\displaystyle A}$), либо содержит единственный элемент (случай, когда ${\displaystyle a_{1}}$ и ${\displaystyle a_{2}}$ — это один и тот же элемент). Вслед за уровнем множеств идёт уровень группоидов (множество точек и множество путей между каждой парой точек), и уровни ${\displaystyle n}$-группоидов всех порядков.

Интуиционистская теория типов	Логика	Теория множеств	Теория гомотопий
тип ${\displaystyle A}$	высказывание ${\displaystyle A}$	множество ${\displaystyle A}$	пространство ${\displaystyle A}$
${\displaystyle a:A}$	доказательство высказывания ${\displaystyle A}$	${\displaystyle a}$ — элемент множества ${\displaystyle A}$	${\displaystyle a}$ — точка пространства ${\displaystyle A}$
зависимый тип ${\displaystyle B(x)}$	предикат ${\displaystyle B(x)}$	семейство множеств	расслоение ${\displaystyle B_{x}}$
${\displaystyle b(x):B(x)}$	условное доказательство	семейство элементов	сечение[англ.]
${\displaystyle \mathbf {0} }$, ${\displaystyle \mathbf {1} }$	${\displaystyle \bot }$, ${\displaystyle \top }$	${\displaystyle \varnothing }$, ${\displaystyle \{\varnothing \}}$	${\displaystyle \varnothing }$, ${\displaystyle \ast }$
${\displaystyle A+B}$	${\displaystyle A\vee B}$	${\displaystyle A\uplus B}$ (дизъюнктное объединение)	${\displaystyle A\oplus B}$ (копроизведение)
${\displaystyle A\times B}$	${\displaystyle A\wedge B}$	${\displaystyle A\times B}$ (декартово произведение)	${\displaystyle A\times B}$ (произведение пространств)
${\displaystyle A\to B}$	${\displaystyle A\Rightarrow B}$	множество функций ${\displaystyle \{f\mid f:A\to B\}}$	функциональное пространство ${\displaystyle B^{A}}$
${\displaystyle {\boldsymbol {\Sigma }}_{x:A}B(x)}$	${\displaystyle \exists _{x:A}B(x)}$	${\displaystyle \biguplus _{x\in A}B(x)}$ (дизъюнктное объединение)	тотальное пространство
${\displaystyle {\boldsymbol {\Pi }}_{x:A}B(x)}$	${\displaystyle \forall _{x:A}B(x)}$	${\displaystyle \prod _{x\in A}B(x)}$ (декартово произведение)	пространство сечений
${\displaystyle {\mathsf {Id}}_{A}}$	равенство (${\displaystyle =}$)	${\displaystyle \{(x,x)\mid x\in A\}}$	пространство путей ${\displaystyle A^{\mathbb {I} }}$

Библиотеки HoTT — несколько проектов, ведущихся на GitHub (в том же репозитории, где и размещены исходные коды книги), в которых создаются формальные описания различных разделов математики средствами систем автоматического доказательства с использованием построений гомотопической теории типов.

В проекте Владимира Воеводского, названном «Библиотека унивалентных оснований»^[6], использовано специально разработанное минимальное безопасное подмножество Coq, обеспечивающее идеологическую чистоту и надёжность построений в согласовании с теорией. Проект HoTT^[7] ведётся стандартными средствами Coq, реализуется в рамках исследовательской программы Института перспективных исследований, и в целом следует книге➤, по состоянию на 2020 год в проекте участвуют 48 разработчиков, наиболее активные — Джейсон Гросс, Майкл Шульман, Али Каглаян и Андрей Бауэр^[8]. Также ведётся параллельный проект на языке Agda^[9].

Существует несколько экспериментальных систем интерактивного доказательства, целиком основанных на HoTT: Arend, RedPRL, redtt, cooltt, а в Agda версии 2.6.0 добавлен так называемый «кубический режим», позволяющий полноценно использовать гомотопические типы.

• Homotopy Type Theory: Univalent Foundations of Mathematics. — Princeton: Institute for Advanced Study, 2013. — 603 p.
• Steve Awodey, Álvaro Pelayo, Michael A. Warren. Voevodsky’s Univalence Axiom in Homotopy Type Theory (англ.) // Notices of the AMS. — 2013. — Vol. 60, no. 9. — P. 1164—1167.
• Hannes Hummel. Will Computers Redefine the Roots of Math? When a legendary mathematician found a mistake in his own work, he embarked on a computer-aided quest to eliminate human error. To succeed, he has to rewrite the century-old rules underlying all of mathematics (англ.). Quanta Magazine^[англ.] (19 мая 2015). Дата обращения: 31 декабря 2017.
• Don Monroe. A new type of mathematics? (англ.) // Communications of the ACM. — 2014. — Vol. 57, no. 2. — P. 13—15. — doi:10.1145/2557446.
• Андрей Родин. Логический и геометрический атомизм от Лейбница до Воеводского // Вопросы философии. — 2016. — № 6. — С. 134—142.

• cs.cmu.edu/~rwh/courses/hott/ — материалы курса по гомотопической теории типов, читаемого Робертом Харпером в Университете Карнеги — Меллон

Для улучшения этой статьи желательно: Проставить сноски, внести более точные указания на источники. Проверить достоверность указанной в статье информации. На странице обсуждения должны быть пояснения. После исправления проблемы исключите её из списка. Удалите шаблон, если устранены все недостатки.