Теория гомотопического типа

Теория типов в логике и математике

Обложка книги «Теория гомотопических типов: унивалентные основы математики» .

В математической логике и информатике теория гомотопических типов ( HoTT ) относится к различным линиям развития интуиционистской теории типов , основанным на интерпретации типов как объектов, к которым применима интуиция (абстрактной) теории гомотопий .

Это включает в себя, среди прочего, построение гомотопических и более высококатегоричных моделей для таких теорий типов; использование теории типов в качестве логики (или внутреннего языка ) для абстрактной гомотопической теории и более высокой теории категорий ; развитие математики в рамках теоретико-типовой основы (включая как ранее существовавшую математику, так и новую математику, которую гомотопические типы делают возможной); и формализацию каждого из них в компьютерных помощниках по доказательству .

Существует большое совпадение между работой, называемой теорией гомотопических типов, и работой, называемой проектом унивалентных оснований . Хотя ни одна из них не очерчена точно, и термины иногда используются взаимозаменяемо, выбор использования также иногда соответствует различиям в точках зрения и акцентах. ^[1] Таким образом, эта статья может не представлять взгляды всех исследователей в этих областях в равной степени. Такого рода изменчивость неизбежна, когда область находится в быстром движении.

История

Группоидная модель

В свое время идея о том, что типы в интенсиональной теории типов с их типами тождества можно рассматривать как группоиды, была математическим фольклором . Впервые она была уточнена семантически в статье 1994 года Мартина Хофманна и Томаса Штрайхера под названием «Модель группоидов опровергает уникальность доказательств тождества» ^[2] , в которой они показали, что интенсиональная теория типов имеет модель в категории группоидов . Это была первая по-настоящему « гомотопическая » модель теории типов, хотя и только «1- мерная » (традиционные модели в категории множеств гомотопически 0-мерны).

Их последующая статья ^[3] предвосхитила несколько более поздних разработок в теории гомотопических типов. Например, они отметили, что модель группоида удовлетворяет правилу, которое они назвали «универсальной экстенсиональностью», что является ничем иным, как ограничением на 1-типы аксиомы однозначности , которую Владимир Воеводский предложил десять лет спустя. (Однако аксиому для 1-типов заметно проще сформулировать, поскольку не требуется связного понятия «эквивалентности».) Они также определили «категории с изоморфизмом как равенство» и предположили, что в модели, использующей многомерные группоиды, для таких категорий будет «эквивалентность есть равенство»; это было позже доказано Бенедиктом Аренсом, Кшиштофом Капулкиным и Майклом Шульманом . ^[4]

Ранняя история: модельные категории и высшие группоиды

Первые многомерные модели теории интенсиональных типов были построены Стивом Аводеем и его студентом Майклом Уорреном в 2005 году с использованием категорий модели Квиллена . Эти результаты были впервые представлены публике на конференции FMCS 2006 ^[5], на которой Уоррен сделал доклад под названием «Гомотопические модели теории интенсиональных типов», который также послужил проспектом его диссертации (в состав диссертационной комиссии входили Аводеем, Никола Гамбино и Алекс Симпсон). Краткое изложение содержится в аннотации проспекта диссертации Уоррена. ^[6]

На последующем семинаре по типам идентичности в Университете Уппсалы в 2006 году ^[7] было два доклада о связи между интенсиональной теорией типов и факторизационными системами: один Ричарда Гарнера, «Системы факторизации для теории типов», ^[8] и один Майкла Уоррена, «Категории моделей и интенсиональные типы идентичности». Связанные идеи обсуждались в докладах Стива Аводи, «Теория типов более высоких размерностей», и Томаса Штрайхера , «Типы идентичности против слабых омега-группоидов: некоторые идеи, некоторые проблемы». На той же конференции Бенно ван ден Берг выступил с докладом под названием «Типы как слабые омега-категории», где он изложил идеи, которые позже стали предметом совместной статьи с Ричардом Гарнером.

Все ранние конструкции многомерных моделей должны были иметь дело с проблемой когерентности, типичной для моделей теории зависимых типов, и были разработаны различные решения. Одно из них было дано в 2009 году Воеводским, другое в 2010 году ван ден Бергом и Гарнером. ^[9] Общее решение, основанное на конструкции Воеводского, в конечном итоге было дано Ламсдейном и Уорреном в 2014 году. ^[10]

На PSSL86 в 2007 году ^[11] Аводей выступил с докладом под названием «Теория гомотопических типов» (это было первое публичное использование этого термина, который был придуман Аводеем ^[12] ). Аводей и Уоррен обобщили свои результаты в статье «Теоретико-гомотопические модели типов идентичности», которая была размещена на сервере препринтов ArXiv в 2007 году ^[13] и опубликована в 2009 году; более подробная версия появилась в диссертации Уоррена «Теоретико-гомотопические аспекты конструктивной теории типов» в 2008 году.

Примерно в то же время Владимир Воеводский независимо исследовал теорию типов в контексте поиска языка для практической формализации математики. В сентябре 2006 года он опубликовал в списке рассылки Types «Очень короткую заметку о гомотопическом лямбда-исчислении » ^[14] , в которой набросал контуры теории типов с зависимыми произведениями, суммами и универсумами и модели этой теории типов в симплициальных множествах Кана . Он начинался словами «Гомотопическое λ-исчисление является гипотетической (на данный момент) системой типов» и заканчивался словами «На данный момент многое из того, что я сказал выше, находится на уровне предположений. Даже определение модели TS в гомотопической категории нетривиально», ссылаясь на сложные проблемы согласованности, которые не были решены до 2009 года. Эта заметка включала синтаксическое определение «типов равенства», которые, как утверждалось, интерпретировались в модели пространствами путей, но не учитывала правила Пера Мартина-Лёфа для типов идентичности. Она также стратифицирует вселенные по гомотопическому измерению в дополнение к размеру, идея, которая позже была в основном отвергнута.

С синтаксической стороны, Бенно ван ден Берг предположил в 2006 году, что башня типов тождества типа в интенсиональной теории типов должна иметь структуру ω-категории, и действительно ω-группоида, в «глобулярном, алгебраическом» смысле Майкла Батанина. Это было позже независимо доказано ван ден Бергом и Гарнером в статье «Типы — слабые омега-группоиды» (опубликованной в 2008 году), ^[15] и Питером Ламсдейном в статье «Слабые ω-категории из интенсиональной теории типов» (опубликованной в 2009 году) и в рамках его докторской диссертации 2010 года «Высшие категории из теорий типов». ^[16]

Аксиома однолистности, синтетическая гомотопическая теория и высшие индуктивные типы

Концепция одновалентного расслоения была введена Воеводским в начале 2006 года. ^[17] Однако из-за настойчивости всех представлений теории типов Мартина-Лёфа на свойстве, что типы тождества в пустом контексте могут содержать только рефлексивность, Воеводский не осознавал до 2009 года, что эти типы тождества могут использоваться в сочетании с одновалентными универсумами. В частности, идея о том, что одновалентность может быть введена просто путем добавления аксиомы к существующей теории типов Мартина-Лёфа, появилась только в 2009 году. ^{[a] [b]}

Также в 2009 году Воеводский разработал больше деталей модели теории типов в комплексах Кана и заметил, что существование универсального расслоения Кана может быть использовано для решения проблем согласованности для категориальных моделей теории типов. Он также доказал, используя идею А. К. Боусфилда, что это универсальное расслоение было однозначным: связанное расслоение парных гомотопических эквивалентностей между слоями эквивалентно расслоению пространства путей базы.

Чтобы сформулировать однозначность как аксиому, Воеводский нашел способ синтаксически определить «эквивалентности», которые имели важное свойство, что тип, представляющий утверждение «f является эквивалентностью», был (при предположении экстенсиональности функции) (-1)-усеченным (т.е. сжимаемым, если обитаем). Это позволило ему дать синтаксическое утверждение однозначности, обобщающее «вселенскую экстенсиональность» Хофмана и Штрайхера на более высокие измерения. Он также смог использовать эти определения эквивалентностей и сжимаемости, чтобы начать разрабатывать значительные объемы «синтетической гомотопической теории» в помощнике по доказательству Coq ; это легло в основу библиотеки, позже названной «Foundations» и в конечном итоге «UniMath». ^[19]

Объединение различных потоков началось в феврале 2010 года с неформальной встречи в Университете Карнеги-Меллона , где Воеводский представил свою модель в комплексах Кана и свой Coq группе, в которую входили Аводей, Уоррен, Ламсдейн, Роберт Харпер , Дэн Ликата, Майкл Шульман и другие. На этой встрече были разработаны наброски доказательства (Уоррена, Ламсдейна, Ликаты и Шульмана) того, что каждая гомотопическая эквивалентность является эквивалентностью (в хорошем когерентном смысле Воеводского), основанной на идее теории категорий об улучшении эквивалентностей до сопряженных эквивалентностей. Вскоре после этого Воеводский доказал, что аксиома однолистности подразумевает экстенсиональность функции.

Следующим ключевым событием стал мини-семинар в Математическом исследовательском институте Обервольфаха в марте 2011 года, организованный Стивом Аводеем, Ричардом Гарнером, Пером Мартином-Лёфом и Владимиром Воеводским, под названием «Гомотопическая интерпретация конструктивной теории типов». ^[20] В рамках руководства по Coq для этого семинара Андрей Бауэр написал небольшую библиотеку Coq ^[21], основанную на идеях Воеводского (но фактически не используя ни одного из его кода); в конечном итоге это стало ядром первой версии библиотеки Coq «HoTT» ^[22] (первый коммит последней ^[23] Майкла Шульмана отмечает «Разработка на основе файлов Андрея Бауэра, со многими идеями, взятыми из файлов Владимира Воеводского»). Одним из самых важных результатов встречи в Обервольфахе стала основная идея высших индуктивных типов, предложенная Ламсдейном, Шульманом, Бауэром и Уорреном. Участники также сформулировали список важных открытых вопросов, таких как: удовлетворяет ли аксиома однолистности условию каноничности (все еще открыт, хотя некоторые особые случаи были решены положительно ^{[24] [25]} ), имеет ли аксиома однолистности нестандартные модели (на которые положительно ответил Шульман), и как определить (полу)симплициальные типы (все еще открыт в MLTT, хотя это можно сделать в системе гомотопических типов Воеводского (HTS), теории типов с двумя типами равенства).

Вскоре после семинара в Обервольфахе был создан веб-сайт и блог Homotopy Type Theory ^[26] , и предмет начал популяризироваться под этим названием. Представление о некоторых важных достижениях в этот период можно получить из истории блога. ^[27]

Унивалентные фундаменты

Фраза «однозначные основания» всеми согласована как тесно связанная с теорией гомотопических типов, но не все используют ее одинаково. Первоначально она была использована Владимиром Воеводским для обозначения его видения фундаментальной системы для математики, в которой базовыми объектами являются гомотопические типы, основанные на теории типов, удовлетворяющей аксиоме однозначности, и формализованные в компьютерном помощнике доказательства. ^[28]

По мере того, как работа Воеводского интегрировалась с сообществом других исследователей, работающих над теорией гомотопических типов, термин «однозначные основания» иногда использовался взаимозаменяемо с термином «гомотопическая теория типов» ^[29] , а в других случаях — только для обозначения его использования в качестве основополагающей системы (за исключением, например, изучения модельно-категориальной семантики или вычислительной метатеории). ^[30] Например, предметом специального года IAS официально было заявлено «однозначные основания», хотя большая часть проделанной там работы была сосредоточена на семантике и метатеории в дополнение к основаниям. Книга, подготовленная участниками программы IAS, была названа «Теория гомотопических типов: однозначные основания математики»; хотя это могло относиться к любому использованию, поскольку в книге HoTT обсуждается только как математическое основание. ^[29]

Специальный год по теме «Унивалентные основы математики»

Анимация, демонстрирующая разработку книги HoTT в репозитории GitHub участниками проекта Univalent Foundations Special Year.

В 2012–13 годах исследователи Института перспективных исследований провели «Специальный год унивалентных оснований математики». ^[31] Специальный год объединил исследователей в области топологии , компьютерных наук , теории категорий и математической логики . Программа была организована Стивом Аводеем , Тьерри Кокандом и Владимиром Воеводским .

В ходе программы Питер Ацель , который был одним из участников, инициировал рабочую группу, которая исследовала, как неформально, но строго заниматься теорией типов, в стиле, аналогичном тому, как обычные математики занимаются теорией множеств. После первоначальных экспериментов стало ясно, что это не только возможно, но и весьма полезно, и что книга (так называемая HoTT Book ) ^{[29] [32]} может и должна быть написана. Затем многие другие участники проекта присоединились к усилиям с технической поддержкой, написанием, корректурой и предложением идей. Необычно для математического текста, что он был разработан совместно и в открытом доступе на GitHub , выпущен под лицензией Creative Commons , которая позволяет людям создавать собственные версии книги, и его можно купить в печатном виде и загрузить бесплатно. ^{[33] [34] [35]}

В более общем плане этот особый год стал катализатором развития всей темы; книга HoTT стала лишь одним, хотя и наиболее заметным, результатом.

Официальные участники особого года

• Питер Ацель
• Бенедикт Аренс
• Торстен Альтенкирх
• Стив Аводей
• Бруно Баррас
• Андрей Бауэр
• Ив Берто
• Марк Безем
• Тьерри Коканд
• Эрик Финстер
• Дэниел Грейсон
• Хьюго Эрбелин
• Андре Джойал
• Дэн Ликата
• Питер Ламсдэйн
• Ассия Махбуби
• Пер Мартин-Лёф
• Сергей Мелихов
• Альваро Пелайо
• Эндрю Полонский
• Майкл Шульман
• Матье Созо
• Бас Спиттерс
• Бенно ван ден Берг
• Владимир Воеводский
• Майкл Уоррен
• Ноам Зейлбергер

ACM Computing Reviews включил книгу в список выдающихся публикаций 2013 года в категории «математика вычислений». ^[36]

Ключевые понятия

«Предложения как типы»

HoTT использует модифицированную версию интерпретации теории типов « предложения как типы », согласно которой типы также могут представлять предложения, а термины могут представлять доказательства. Однако в HoTT, в отличие от стандартных «предложений как типов», особую роль играют «простые предложения», которые, грубо говоря, являются типами, имеющими не более одного термина, вплоть до пропозиционального равенства . Они больше похожи на обычные логические предложения, чем на общие типы, в том смысле, что они не имеют отношения к доказательству.

Равенство

Фундаментальным понятием теории гомотопических типов является путь . В HoTT тип — это тип всех путей из точки в точку . (Следовательно, доказательство того, что точка равна точке, — это то же самое, что и путь из точки в точку .) Для любой точки существует путь типа , соответствующий рефлексивному свойству равенства. Путь типа может быть инвертирован, образуя путь типа , соответствующий симметричному свойству равенства. Два пути типа соответственно могут быть объединены, образуя путь типа ; это соответствует транзитивному свойству равенства. ${\displaystyle a=b}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a}$ ${\displaystyle a=a}$ ${\displaystyle a=b}$ ${\displaystyle b=a}$ ${\displaystyle a=b}$ ${\displaystyle b=c}$ ${\displaystyle a=c}$

Самое важное, учитывая путь и доказательство некоторого свойства , доказательство может быть «перенесено» по пути, чтобы получить доказательство свойства . (Эквивалентно, объект типа может быть превращен в объект типа .) Это соответствует свойству подстановки равенства . Здесь проявляется важное различие между HoTT и классической математикой. В классической математике, как только установлено равенство двух значений и , и могут впоследствии использоваться взаимозаменяемо, без учета каких-либо различий между ними. Однако в теории гомотопических типов может быть несколько различных путей , и перемещение объекта по двум различным путям даст два разных результата. Поэтому в теории гомотопических типов при применении свойства подстановки необходимо указать, какой путь используется. ${\displaystyle p:a=b}$ ${\displaystyle P(a)}$ ${\displaystyle p}$ ${\displaystyle P(b)}$ ${\displaystyle P(a)}$ ${\displaystyle P(b)}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a=b}$

В общем случае, «предложение» может иметь несколько различных доказательств. (Например, тип всех натуральных чисел, рассматриваемый как предложение, имеет каждое натуральное число в качестве доказательства.) Даже если предложение имеет только одно доказательство , пространство путей может быть нетривиальным в некотором роде. «Простое предложение» — это любой тип, который либо пуст, либо содержит только одну точку с тривиальным пространством путей . ${\displaystyle a}$ ${\displaystyle a=a}$

Обратите внимание, что люди пишут для , тем самым оставляя тип неявным . Не путайте его с , обозначающим функцию тождества на . ^[c] ${\displaystyle a=b}$ ${\displaystyle Id_{A}(a,b)}$ ${\displaystyle A}$ ${\displaystyle a,b}$ ${\displaystyle id_{A}:A\to A}$ ${\displaystyle A}$

Эквивалентность типов

Два типа и принадлежащие к некоторому универсуму определяются как эквивалентные , если между ними существует эквивалентность . Эквивалентность — это функция ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle U}$

${\displaystyle f:A\to B}$

который имеет как левый обратный, так и правый обратный, в том смысле, что при подходящем выборе и оба следующих типа являются обитаемыми: ${\displaystyle g}$ ${\displaystyle h}$

${\displaystyle Id_{B\rightarrow B}(f\circ g,id_{B}),}$

${\displaystyle Id_{A\rightarrow A}(h\circ f,id_{A}).}$

то есть

${\displaystyle f\circ g=_{B\rightarrow B}id_{B},}$

${\displaystyle h\circ f=_{A\rightarrow A}id_{A}.}$

Это выражает общее понятие " имеет как левый обратный, так и правый обратный", используя типы равенства. Обратите внимание, что условия обратимости выше являются типами равенства в типах функций и . Обычно предполагается аксиома экстенсиональности функции, которая гарантирует, что они эквивалентны следующим типам, которые выражают обратимость, используя равенство в области и кодомене и : ${\displaystyle f}$ ${\displaystyle A\rightarrow A}$ ${\displaystyle B\rightarrow B}$ ${\displaystyle A}$ ${\displaystyle B}$

${\displaystyle \Pi _{y:B}.\ Id_{B}((f\circ g)(y),id_{B}(y)),}$

${\displaystyle \Pi _{x:A}.\ Id_{A}((h\circ f)(x),id_{A}(x)).}$

т.е. для всех и , ${\displaystyle x:A}$ ${\displaystyle y:B}$

${\displaystyle f(g(y))=_{B}y,}$

${\displaystyle h(f(x))=_{A}x.}$

Функции типа

${\displaystyle A\to B}$

вместе с доказательством того, что они являются эквивалентностями, обозначаются как

${\displaystyle A\simeq B}$.

Аксиома однозначности

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

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

что выражает , в частности, то, что типы, которые равны, также эквивалентны. ${\displaystyle A,B}$

Аксиома однозначности утверждает, что эта функция сама по себе является эквивалентностью. ^{[29] : 115  [18] : 4–6} Следовательно, мы имеем

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

«Другими словами, тождественность эквивалентна эквивалентности. В частности, можно сказать, что «эквивалентные типы идентичны». ^{[29] : 4}

Мартин Хетцель Эскардо показал, что свойство однозначности не зависит от теории типов Мартина-Лёфа (MLTT). ^{[18] : 6  [d]}

Приложения

Доказательство теоремы

Сторонники утверждают, что HoTT позволяет переводить математические доказательства на язык программирования для помощников по компьютерному доказательству гораздо проще, чем раньше. Они утверждают, что этот подход увеличивает потенциал компьютеров для проверки сложных доказательств. ^[37] Однако эти утверждения не являются общепринятыми, и многие исследовательские работы и помощники по доказательству не используют HoTT.

HoTT принимает аксиому однозначности, которая связывает равенство логико-математических предложений с теорией гомотопии. Уравнение, такое как является математическим предложением, в котором два разных символа имеют одинаковое значение. В теории гомотопических типов это означает, что две формы, представляющие значения символов, топологически эквивалентны. ^[37] ${\displaystyle a=b}$

Эти отношения эквивалентности, утверждает директор Института теоретических исследований ETH Zürich Джованни Фелдер , могут быть лучше сформулированы в теории гомотопии, поскольку она более всеобъемлюща: Теория гомотопии объясняет не только, почему «a равно b», но и как это вывести. В теории множеств эта информация должна быть определена дополнительно, что, как утверждают сторонники, затрудняет перевод математических предложений на языки программирования. ^[37]

Компьютерное программирование

По состоянию на 2015 год велась интенсивная исследовательская работа по моделированию и формальному анализу вычислительного поведения аксиомы однолистности в теории гомотопических типов. ^[38]

Теория кубического типа — это одна из попыток придать вычислительное содержание теории гомотопического типа. ^[39]

Однако считается, что некоторые объекты, такие как полусимплициальные типы, не могут быть построены без ссылки на некоторое понятие точного равенства. Поэтому были разработаны различные двухуровневые теории типов , которые разделяют свои типы на фибрантные типы, которые учитывают пути, и нефибрантные типы, которые не учитывают. Декартова кубическая вычислительная теория типов является первой двухуровневой теорией типов, которая дает полную вычислительную интерпретацию теории гомотопических типов. ^[40]

Смотрите также

• Исчисление конструкций
• Переписка Карри–Говарда
• Интуиционистская теория типов
• Гипотеза гомотопии
• Унивалентные фундаменты

Примечания

1. Унивалентность — это тип, свойство типа идентичности IdU вселенной U — Мартин Хётцель Эскардо (2018) ^{[18] : стр.1}
2. "Унивалентность — это тип, а аксиома унивалентности гласит, что этот тип имеет некоторого обитателя." ^{[18] : стр.1}
3. Здесь используется соглашение теории типов, согласно которому имена типов начинаются с заглавной буквы, а имена функций — со строчной буквы.
4. Мартин Хётцель Эскардо показал, что свойство одновалентности, «свойство типа тождества IdU универсума U», ^{[18] : 4} может иметь или не иметь жителя. По аксиоме одновалентности тип 'isUnivalent(U)' имеет жителя; Хётцель Эскардо отмечает, что когда отражение является единственным способом построения элементов типа тождества, отличным от одновалентности, можно построить функцию J из типа тождества, из отражения и из J. ^{[18] : 2.4 Тип тождества} Хётцель Эскардо приступает к построению типа одновалентности, используя повторные применения J. Когда 'все типы являются множествами' (обозначается аксиомой K), ^{[18] : 2.4} Аксиома K подразумевает, что тип 'isUnivalent(U)' не имеет жителя. Таким образом, Хетцель Эскардо обнаруживает, что тип isUniвалент(U) не определен в Теории типов Мартина-Лёфа (MLTT). ^{[18] : 3.2, с.6 Аксиома однолистности}

Ссылки

1. Шульман, Майкл (27 января 2016 г.). «Теория гомотопических типов: синтетический подход к высшим равенствам». arXiv : 1601.05035v3 [math.LO]., сноска 1
2. Хофманн, М.; Штрейхер, Т. (1994). «Модель группоида опровергает уникальность доказательств тождества». Труды Девятого ежегодного симпозиума IEEE по логике в компьютерных науках . С. 208–212. doi :10.1109/LICS.1994.316071. ISBN 0-8186-6310-3. S2CID  19496198.
3. Хофманн, Мартин; Штрейхер, Томас (1998). «Группоидная интерпретация теории типов». В Самбин, Джованни; Смит, Ян М. (ред.). Двадцать пять лет конструктивной теории типов . Oxford Logic Guides. Том 36. Clarendon Press. С. 83–111. ISBN 978-0-19-158903-4. МР  1686862.
4. Аренс, Бенедикт; Капулкин, Кшиштоф; Шульман, Майкл (2015). «Унивалентные категории и пополнение Резка». Математические структуры в информатике . 25 (5): 1010–1039. arXiv : 1303.0584 . doi :10.1017/S0960129514000486. MR  3340533. S2CID  1135785.
5. "Foundational Methods in Computer Science 2006, University of Calgary, 7–9 июня 2006 г.". University of Calgary . Получено 6 июня 2021 г. .
6. Уоррен, Майкл А. (2006). Гомотопические модели теории интенсиональных типов (PDF) (диссертация).
7. "Типы тождественности - топологическая и категориальная структура, семинар, Уппсала, 13-14 ноября 2006 г.". Университет Уппсалы - Кафедра математики . Получено 6 июня 2021 г.
8. Ричард Гарнер, Аксиомы факторизации для теории типов
9. Берг, Бенно ван ден; Гарнер, Ричард (27 июля 2010 г.). «Топологические и симплициальные модели типов тождеств». arXiv : 1007.4638 [math.LO].
10. Ламсдейн, Питер ЛеФану; Уоррен, Майкл А. (6 ноября 2014 г.). «Модель локальных вселенных: упущенная из виду конструкция когерентности для зависимых теорий типов». Труды ACM по вычислительной логике . 16 (3): 1–31. arXiv : 1411.1736 . doi : 10.1145/2754931. S2CID  14068103.
11. "86-е издание перипатетического семинара по пучкам и логике, Университет Анри Пуанкаре, 8-9 сентября 2007 г.". loria.fr. Архивировано из оригинала 17 декабря 2014 г. Получено 20 декабря 2014 г.
12. Предварительный список участников PSSL86
13. Awodey, Steve; Warren, Michael A. (3 сентября 2007 г.). "Гомотопические теоретические модели типов идентичности". Математические труды Кембриджского философского общества . 146 (1): 45. arXiv : 0709.0248 . Bibcode : 2008MPCPS.146...45A. doi : 10.1017/S0305004108001783. S2CID  7915709.
14. Воеводский, Владимир (27 сентября 2006 г.). «Очень короткая заметка о гомотопическом λ-исчислении». ucr.edu . Получено 6 июня 2021 г. .
15. Ван ден Берг, Бенно; Гарнер, Ричард (1 декабря 2007 г.). «Типы — слабые омега-группоиды». Труды Лондонского математического общества . 102 (2): 370–394. arXiv : 0812.0298 . doi : 10.1112/plms/pdq026. S2CID  5575780.
16. Lumsdaine, Peter (2010). "Higher Categories from Type Theories" (PDF) (Ph.D.). Carnegie Mellon University. Архивировано из оригинала (PDF) 21 декабря 2014 года . Получено 21 декабря 2014 года .
17. Заметки о гомотопическом лямбда-исчислении, март 2006 г.
18. Мартин Хетцель Эскардо (18 октября 2018 г.) Самостоятельная, краткая и полная формулировка аксиомы однолистности Воеводского.
19. Репозиторий GitHub, Univalent Mathematics
20. Аводей, Стив; Гарнер, Ричард; Мартин-Лёф, Пер; Воеводский, Владимир (27 февраля – 5 марта 2011 г.). «Мини-семинар: интерпретация гомотопии конструктивной теории типов» (PDF) . Oberwolfach Reports . 8 . Mathematical Research Institute of Oberwolfach: 609–638. doi :10.4171/OWR/2011/11 . Получено 6 июня 2021 г. .
21. Репозиторий GitHub, Андрей Бауэр, Теория гомотопии в Coq
22. Бауэр, Андрей; Воеводский Владимир (29 апреля 2011 г.). «Основная теория гомотопических типов». Гитхаб . Проверено 6 июня 2021 г.
23. Репозиторий GitHub, Теория гомотопических типов
24. Шульман, Майкл (2015). «Унивалентность для обратных диаграмм и гомотопическая каноничность». Математические структуры в информатике . 25 (5): 1203–1277. arXiv : 1203.3253 . doi :10.1017/S0960129514000565. S2CID  13595170.
25. Ликата, Дэниел Р.; Харпер, Роберт (21 июля 2011 г.). «Каноничность для теории двумерных типов» (PDF) . Университет Карнеги — Меллона . Получено 6 июня 2021 г. .
26. Теория гомотопических типов и унивалентные основы Блог
27. Блог теории гомотопических типов
28. Теория типов и унивалентные основания
29. Программа унивалентных оснований (2013). Теория гомотопических типов: унивалентные основания математики. Институт перспективных исследований.
30. Теория гомотопических типов: Ссылки
31. Математическая школа IAS: Специальный год по теме «Унивалентные основания математики»
32. Официальное объявление о книге HoTT, Стив Аводей, 20 июня 2013 г.
33. Монро, Д. (2014). «Новый тип математики?». Comm ACM . 57 (2): 13–15. doi :10.1145/2557446. S2CID  6120947.
34. Шульман, Майк (20 июня 2013 г.). «The HoTT Book». The n-Category Café . Получено 6 июня 2021 г. – через Техасский университет.
35. Бауэр, Андрей (20 июня 2013 г.). «The HoTT Book». Математика и вычисления . Получено 6 июня 2021 г. .
36. ACM Computing Reviews . «Лучшее за 2013 год».
37. Meyer, Florian (3 сентября 2014 г.). «Новый фундамент для математики». R&D Magazine . Получено 29 июля 2021 г.
38. Соякова, Кристина (2015). Высшие индуктивные типы как гомотопически-инициальные алгебры. POPL 2015. arXiv : 1402.0761 . doi :10.1145/2676726.2676983.
39. Коэн, Сирил; Коканд, Тьерри; Хубер, Саймон; Мёртберг, Андерс (2015). Теория кубических типов: конструктивная интерпретация аксиомы однозначности. ТИПЫ 2015.
40. Ангили, Карло; Фавония; Харпер, Роберт (2018). Декартова кубическая теория вычислительных типов: конструктивное рассуждение с путями и равенствами (PDF) . Computer Science Logic 2018. Получено 26 августа 2018 г.(появиться)

Библиография

• Программа унифицированных оснований (2013). Теория гомотопических типов: унифицированные основания математики. Принстон, Нью-Джерси: Институт перспективных исследований . MR  3204653.(В этой статье указана версия GitHub.)
• Awodey, S. ; Warren, MA (январь 2009 г.). «Теоретические модели гомотопий типов тождества». Математические труды Кембриджского философского общества . 146 (1): 45–55. arXiv : 0709.0248 . Bibcode :2008MPCPS.146...45A. doi :10.1017/S0305004108001783. S2CID  7915709.В формате PDF.
• Awodey, Steve (2012). "Теория типов и гомотопия" (PDF) . В Dybjer, P.; Lindström, Sten; Palmgren, Erik; et al. (ред.). Эпистемология против онтологии . Логика, эпистемология и единство науки. Springer. стр. 183–201. CiteSeerX  10.1.1.750.3626 . doi :10.1007/978-94-007-4435-6_9. ISBN 978-94-007-4434-9. S2CID  4499538.
• Awodey, Steve (2014). «Структурализм, инвариантность и однозначность». Philosophia Mathematica . 22 (1): 1–11. CiteSeerX  10.1.1.691.8113 . doi :10.1093/philmat/nkt030.
• Хофманн, Мартин; Штрейхер, Томас (1998). «Группоидная интерпретация теории типов». В Sambin, G.; Smith, JM (ред.). Двадцать пять лет конструктивной теории типов . Clarendon Press. стр. 83–112. ISBN 978-0-19-158903-4.В качестве постскриптума.
• Рийке, Эгберт (2012). Гомотопическая теория типов (PDF) (магистратура). Утрехтский университет.
• Воеводский, Владимир (2006), Очень краткая заметка о гомотопическом лямбда-исчислении (PDF)
• Воеводский, Владимир (2010), Аксиома эквивалентности и унивалентные модели теории типов , arXiv : 1402.5556 , Bibcode : 2014arXiv1402.5556V
• Уоррен, Майкл А. (2008). Гомотопические теоретические аспекты конструктивной теории типов (PDF) (Ph.D.). Университет Карнеги-Меллона.

Дальнейшее чтение

• Дэвид Корфилд (2020), Теория модальных гомотопических типов: перспективы новой логики для философии , Oxford University Press.
• Эгберт Рийке (2022), Введение в теорию гомотопических типов , arXiv :2212.11082. Вводный учебник.

Внешние ссылки

• Теория гомотопических типов
• Теория гомотопического типа в n Lab
• Теория гомотопического типа вики
• Веб-страница Владимира Воеводского о Единых Основаниях
• Теория гомотопических типов и унифицированные основы математики Стива Аводея
• «Конструктивная теория типов и гомотопия» – Видеолекция Стива Аводея в Институте перспективных исследований

Библиотеки формализованной математики

• Библиотека фондов (2010-настоящее время)
• Библиотека HoTT (2011-настоящее время), 30 января 2022 г.
• Библиотека P-adics (2011-2012)
• Библиотека RezkCompletion, январь 2022 г.(теперь интегрирован в UniMath, где происходит дальнейшая разработка)
• Библиотека теории К
• Библиотека UniMath (2014-настоящее время), 25 января 2022 г.