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

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

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

Ключевая идея теории — аксиома унивалентности, постулирующая равенство объектов, между которыми может быть установлена эквивалентность, то есть, в гомотопической теории типов как равные рассматриваются изоморфные, гомеоморфные, гомотопически эквивалентные структуры; эта аксиома отражает важные свойства интерпретации высшей категории, а также обеспечивает техническое упрощение формального языка.
Q1056428
теории типов
Concept
Q217413
теории категорий
Concept
Q212803
алгебраической топологии
Concept
Q579978
гомологической алгебры
Concept
Q746083
гомотопическом типе
Concept
Q1166618
логике
Concept
Q9143
языках программирования
Concept
Q1137814
конструктивными
Concept
Q431667
автоматической проверки
Concept
Q68
компьютер
Concept
Q369662
Владимиром Воеводским
PER
None
UniMath
UNK
Q11538
Математическое доказательство
Concept
Q975734
изоморфизма Карри — Ховарда
Concept
Q5891840
Гомотопическая теория типов
Concept
subclass of