Гомотопическая теория типов (HoTT, от ) — математическая теория, особый вариант теории типов, снабжённый понятиями из теории категорий, алгебраической топологии, гомологической алгебры; базируется на взаимосвязи между понятиями о гомотопическом типе пространства, и типах в логике и языках программирования.
Унивалентные основания математики — программа построения средствами гомотопической теории типов универсального формального языка, являющегося конструктивными основаниями для современных разделов математики и обеспечивающего возможность автоматической проверки правильности доказательств на компьютере. Инициирована Владимиром Воеводским в конце 2000-х годов; толчком к более широкому интересу к унивалентным основаниям послужила написанная Воеводским библиотека формализованной математики «Foundations», ставшая к середине 2010-х годов частью библиотеки UniMath и послужившая основой для многих других библиотек; в рамках программы большим коллективом математиков была написана книга.
Математическое доказательство в гомотопической теории типов состоит в установлении «обитаемости» необходимого типа, то есть, в построении выражения соответствующего типа. Использование систем автоматического доказательства для теории эксплуатирует идею изоморфизма Карри — Ховарда, а благодаря математическому содержанию, вложенному в теоретико-типовые понятия, на формальном языке теории удаётся выразить и проверить достаточно сложные результаты из абстрактных разделов математики, которые ранее считались не формализуемыми программными средствами.
Ключевая идея теории — аксиома унивалентности, постулирующая равенство объектов, между которыми может быть установлена эквивалентность, то есть, в гомотопической теории типов как равные рассматриваются изоморфные, гомеоморфные, гомотопически эквивалентные структуры; эта аксиома отражает важные свойства интерпретации высшей категории, а также обеспечивает техническое упрощение формального языка.
История Идея использования интуиционистской теории типов Пера Мартин-Лёфа для формализации высших категорий восходит к работе , в которой была построена система FOLDS (). Ключевым отличием унивалентных оснований от идей Маккаи является принцип, согласно которому фундаментальными объектами математики являются не высшие категории, а высшие группоиды. Поскольку высшие группоиды отвечают по соответствию Гротендика гомотопическим типам, можно сказать, что математика, с точки зрения унивалентных оснований, изучает структуры на гомотопических типах. Возможность прямого использования теории типов Мартин-Лёфа для описания структур на гомотопических типах является следствием построения Воеводским унивалентной модели теории типов. Построение этой модели требовало решения многочисленных технических проблем связанных с так называемыми свойствами когерентности и, хотя основные идеи унивалентных оснований были сформулированны им в 2005—2006 годы, полная унивалентная модель в категории симплициальных множеств появилась только в 2009 году. В те же годы, что и эти исследования Воеводского, велись и другие работы по изучению различных связей между теорией типов и теорией гомотопий, в частности, одним из исторически важных событий, собравшим учёных, работавших в этом направлении, стал семинар в Уппсале в ноябре 2006 года.
В феврале 2010 года Воеводский начал создавать библиотеку на Coq, выросшую впоследствии в совместно разрабатываемую широким кругом учёных «библиотеку унивалентных оснований».
По инициативе Воеводского, 2012—2013 академический год в Институте перспективных исследований был объявлен «годом унивалентных оснований», в сотрудничестве с Ауди и Коканом была открыта специальная исследовательская программа и в её рамках группа из математиков и специалистов по информатике работали над развитием теории. Одним из результатов года стало совместное создание участниками шестисотстраничной книги «Гомотопическая теория типов: унивалентные основания математики», выложенной на сайте программы в свободный доступ под лицензией CC-SA; для совместной работы над книгой был создан проект на GitHub.
Участники программы, представленные во введении к книге:
Бенедикт Аренс (Benedikt Ahrens)
Брюно Баррас (Bruno Barras)
Марк Безем (Marc Bezem) Ив Берто (Yves Bertot) Бенно ван ден Берг (Benno van den Berg) Владимир Воеводский Дэниэл Грейсон (Daniel Grayson, создатель системы компьютерной алгебры )
Тьерри Кокан Дэн Ликата (Dan Licata) Питер Лумсдейн (Peter Lumsdaine) Пер Мартин-Лёф Ассайя Махбуби (Assia Mahboubi) Сергей Мелихов Альваро Пелайо (Alvaro Pelayo) Эндрю Полонский (Andrew Polonsky) Матье Созо (Matthieu Sozeau) Бас Спиттерс (Bas Spitters) Майкл Уоррен (Michael Warren) Эрик Финстер (Eric Finster) Ноам Цейльбергер (Noam Zeilberger)
Юго Эрбелен (Hugo Herbelin, менеджер проекта разработки Coq)
Кроме того, во введении указано, что значительный вклад внесли также шестеро студентов, а также отмечен вклад более 20-ти учёных и практиков, посетивших в течение «года унивалентых оснований» Институт высших исследований (среди которых создатель семантики λ-исчисления Дана Скотт и разработчик формализаций на Coq доказательств задачи о четырёх красках и теоремы Фейта — Томпсона ). Книга построена из двух частей — «Основания» и «Математика», в первой части излагаются основные положения и определяется инструментарий, во второй — строятся реализации введёнными средствами теории гомотопий, теории категорий, теории множеств, вещественных чисел.
Основные положения Теория основывается на интенсиональном варианте интуиционистской теории типов Мартин-Лёфа и использует интерпретацию типов как объектов теории гомотопий и высших категорий. Так, с этой точки зрения отношение принадлежности точки пространству рассматривается как терм соответствующего типа: , расслоение с базой — как зависимый тип . При этом отпадает необходимость представлять пространства в виде множеств точек, снабжённых топологией, и представлять непрерывные отображения между пространствами — как функции сохраняющие или отражающие соответствующие поточечные свойства пространств. Гомотопическая теория типов рассматривает пространства-типы и термы этих типов (точки) как элементарные понятия, а конструкции над пространствами, такие как гомотопии и расслоения, — как зависимые типы.
В формальном построении теории типов используется тип-универсум , термы которого — все прочие неуниверсальные («малые») типы, далее строятся типы такие, что , притом все термы типа также являются термами типа . Зависимые типы (семейства типов) определяются как функции , кообласть которых — некоторый тип-универсум.
В гомотопической теории типов существует несколько способов конструирования новых типов из уже имеющихся. Базовые примеры такого рода — -типы (зависимые функциональные типы, типы-произведения) и -типы (зависимые типы-суммы). Для данного типа и семейства можно построить тип , термы которого — функции, кообласть которых зависит от элемента области определения (геометрически такие функции можно представлять как сечения некоторого расслоения), а также тип , термы которого геометрически соответствуют элементам тотального пространства расслоения.
Равенство термов одного и того же типа в гомотопической теории типов может быть либо равенством «по определению» (), либо пропозициональным равенством. Равенство по определению влечёт пропозициональное равенство, но не наоборот. В общем случае, пропозициональное равенство термов и типа представляется в виде непустого типа , который называют типом тождества; термы этого последнего типа — это пути вида в пространстве ; тип тождества , таким образом, рассматривается как пространство путей (то есть непрерывных отображений единичного отрезка в ) из точки в точку .
Аксиома унивалентности Интуиционистская теория типов позволяет определить понятие эквивалентности типов (для типов принадлежащих одному универсуму) и построить каноническим образом функцию из типа тождества в тип эквивалентности : .
Аксиома унивалентности, сформулированная Воеводским, утверждает, что эта функция также является эквивалентностью: ,
то есть, тип тождества двух данных типов эквивалентен типу эквивалентности этих типов. В случае если и — пропозициональные типы, аксиома имеет особенно прозрачный смысл и сводится к утверждению, который иногда называют принципом экстенсиональности Чёрча: равенство высказываний логически эквивалентно их логической эквивалентности; использование этого принципа означает, что во внимание принимаются только истинностные значения высказываний, но не их смысл. Следствием аксиомы является , то есть утверждение о том, что функции, значения которых равны для всех равных значений их аргументов, равны между собой. Это свойство функций имеет важное значение в информатике.
Аксиома рассматривается некоторыми философами математики в качестве точной математической формулировки основного тезиса философии , которая опирается на распространённую практику математических рассуждений «с точностью до изоморфизма» или «с точностью до эквивалентности».
Логика, множества, группоиды Высказывание (, «голое высказывание») в гомотопической теории типов определяется как тип , который либо пуст, либо содержит единственный терм ; такие типы называются пропозициональными. Если тип пуст, то соответствующее высказывание ложно, если содержит терм (символически — ), то соответствующее высказывание истинно, а терм рассматривается как его доказательство. Таким образом, в теории используется интуиционистская концепция истины, согласно которой истинность высказывания понимается как возможность предъявить доказательство этого высказывания.
Фрагмент гомотопической теории типов, который ограничивается операциями с пропозициональными типами, то есть с высказываниями, можно описать как логический фрагмент (логику) этой теории. Логическая дизъюнкция соответствует в пропозициональном фрагменте типу-сумме , конъюнкция — типу-произведению , импликация — функциональному типу , отрицание — типу , где — это пустой тип (нуль-тип). Логика, соответствующая таким конструкциям, является вариантом интуиционистской логики, в частности, в ней не имеют места такие утверждения, как закон двойного отрицания или исключённого третьего.
Всякий тип , который содержит два или больше различных термов может быть поставлен в однозначное соответствие с пропозициональным типом, который получается в результате отождествления всех термов типа , такая операция называется пропозициональным обрезанием (). Это позволяет провести различие между «пропозициональным уровнем» (уровнем высказываний) теории и гомотопической иерархии «высших» непропозициональных её уровней.
За уровнем высказываний следует уровень множеств. Множество в гомотопической теории типов определяется как пространство (тип) с дискретной топологией. Эквивалентно, множество можно описать в теории как тип, такой что для любых его термов тип является высказыванием, то есть либо пуст (случай когда и — это различные элементы множества ), либо содержит единственный элемент (случай, когда и — это один и тот же элемент). Вслед за уровнем множеств идёт уровень группоидов (множество точек и множество путей между каждой парой точек), и уровни -группоидов всех порядков.
Различные интерпретации теоретико-типовых понятий Интуиционистская теория типов Логика Теория множеств Теория гомотопий тип высказывание множество пространство доказательство высказывания — элемент множества — точка пространства зависимый тип предикат семейство множеств расслоение условное доказательство семейство элементов , , , ,
(дизъюнктное объединение) (копроизведение)
(декартово произведение) (произведение пространств)
множество функций функциональное пространство
(дизъюнктное объединение) тотальное пространство
(декартово произведение) пространство сечений равенство ()
пространство путей
Библиотеки и реализации HoTT