In mathematical logic and computer science, homotopy type theory (HoTT /hɒt/) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies. This includes, among other lines of work, the construction of homotopical and higher-categorical models for such type theories; the use of type theory as a logic (or internal language) for abstract homotopy theory and higher category theory; the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible); and the formalization of each of these in computer proof assistants. There is a large overlap between the work referred to as homotopy type theory, and as the univalent foundations project. Although neither is precisely delineated, and the terms are sometimes used interchangeably, the choice of usage also sometimes corresponds to differences in viewpoint and emphasis. As such, this article may not represent the views of all researchers in the fields equally. This kind of variability is unavoidable when a field is in rapid flux. (en)
En lógica matemática y ciencias de la computación, la teoría de tipos homotópica (HoTT /hɒt/, por sus siglas en inglés) son varias líneas de desarrollo de la teoría de tipos intensional, basada en interpretar los tipos como objetos a los cuales se aplican las intuiciones de la teoría de homotopía abstracta. Esto incluye, entre otras líneas de trabajo, la construcción de modelos homotópicos y en teorías de categorías de alto orden para las teorías de tipos intensionales; el uso de la teoría de tipos como lógica (o lenguaje interno) de la teoría de homotopía abstracta y teoría de categorías de orden superior; el desarrollo de matemáticas dentro de fundaciones basadas en teoría de tipos (incluyendo tanto matemática existente como la matemática nueva que los tipos homotópicos hacen posible); y la formalización de cada una de estas líneas en asistentes de demostración. (es)
Dans la logique mathématique et de l’informatique, la théorie des types homotopiques (en anglais : Homotopy Type Theory HoTT) fait référence à différentes lignes de développement de la théorie des types intuitionnistes, basée sur l’interprétation des types comme des objets auxquels l’intuition de la théorie de l’homotopie s’applique. Cela inclut, entre autres travaux, la construction de modèles homotopiques et de modèles de pour de telles théories de types, l’utilisation de la théorie des types en tant que logique pour la théorie de l’homotopie et la théorie des catégories supérieures, le développement des mathématiques dans une base théorique de type (incluant à la fois les mathématiques existantes et les mathématiques rendues possibles par les types homotopiques), et la formalisation de chacune d’elles en assistants de preuve informatique. Il existe un important chevauchement entre les travaux associés à la théorie des types homotopiques et ceux qui se réfèrent au projet des fondations univalentes. Bien que ni l’un ni l’autre ne soient définis avec précision et que les termes soient parfois utilisés de manière interchangeable, l’utilisation correspond parfois à des différences de points de vue et de priorités. En tant que tel, cet article peut ne pas représenter de manière égale les points de vue de tous les chercheurs dans ces domaines. Ce type de variabilité est inévitable lorsqu’un champ est en pleine évolution. (fr)
Гомотопическая теория типов (HoTT, от англ. homotopy type theory) — математическая теория, особый вариант теории типов, снабжённый понятиями из теории категорий, алгебраической топологии, гомологической алгебры; базируется на взаимосвязи между понятиями о гомотопическом типе пространства, и типах в логике и языках программирования. Унивалентные основания математики — программа построения средствами гомотопической теории типов универсального формального языка, являющегося конструктивными основаниями для современных разделов математики и обеспечивающего возможность автоматической проверки правильности доказательств на компьютере. Инициирована Владимиром Воеводским в конце 2000-х годов; толчком к более широкому интересу к унивалентным основаниям послужила написанная Воеводским библиотека формализованной математики «Foundations», ставшая к середине 2010-х годов частью библиотеки и послужившая основой для многих других библиотек; в рамках программы большим коллективом математиков была написана книга. Математическое доказательство в гомотопической теории типов состоит в установлении «обитаемости» необходимого типа, то есть, в построении выражения соответствующего типа. Использование систем автоматического доказательства для теории эксплуатирует идею изоморфизма Карри — Ховарда, а благодаря математическому содержанию, вложенному в теоретико-типовые понятия, на формальном языке теории удаётся выразить и проверить достаточно сложные результаты из абстрактных разделов математики, которые ранее считались не формализуемыми программными средствами. Ключевая идея теории — аксиома унивалентности, постулирующая равенство объектов, между которыми может быть установлена эквивалентность, то есть, в гомотопической теории типов как равные рассматриваются изоморфные, гомеоморфные, гомотопически эквивалентные структуры; эта аксиома отражает важные свойства интерпретации высшей категории, а также обеспечивает техническое упрощение формального языка. (ru)
在数理逻辑与计算机科学中，同伦类型论（homotopy type theory，缩写 HoTT）是一套旨在于同伦论的大框架下构建内涵类型论语义的理论，尤指和。反而言之，内涵类型论则为同伦理论提供了一套逻辑语言。类型论在绝大多数计算机证明辅助系统中被用作集合论的替代理论，因为集合论的语言难以转化成计算机证明辅助的形式语言。 (zh)
在数理逻辑与计算机科学中，同伦类型论（homotopy type theory，缩写 HoTT）是一套旨在于同伦论的大框架下构建内涵类型论语义的理论，尤指和。反而言之，内涵类型论则为同伦理论提供了一套逻辑语言。类型论在绝大多数计算机证明辅助系统中被用作集合论的替代理论，因为集合论的语言难以转化成计算机证明辅助的形式语言。 (zh)
In mathematical logic and computer science, homotopy type theory (HoTT /hɒt/) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies. (en)
En lógica matemática y ciencias de la computación, la teoría de tipos homotópica (HoTT /hɒt/, por sus siglas en inglés) son varias líneas de desarrollo de la teoría de tipos intensional, basada en interpretar los tipos como objetos a los cuales se aplican las intuiciones de la teoría de homotopía abstracta. (es)
Dans la logique mathématique et de l’informatique, la théorie des types homotopiques (en anglais : Homotopy Type Theory HoTT) fait référence à différentes lignes de développement de la théorie des types intuitionnistes, basée sur l’interprétation des types comme des objets auxquels l’intuition de la théorie de l’homotopie s’applique. (fr)
Гомотопическая теория типов (HoTT, от англ. homotopy type theory) — математическая теория, особый вариант теории типов, снабжённый понятиями из теории категорий, алгебраической топологии, гомологической алгебры; базируется на взаимосвязи между понятиями о гомотопическом типе пространства, и типах в логике и языках программирования. (ru)