vignette| Couverture de Homotopy type Theory: Univalent Foundations of Mathematics. Dans la logique mathématique et de l'informatique, la théorie homotopique des types ou plus exactement la théorie des types d'homotopie (en anglais Homotopy Type Theory, ou 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 catégories supérieures 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 homotopique des types 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.
Histoire
Préhistoire : le modèle du groupoïde Dans les années 1990, que les types de la , avec leurs types identité, soient considérés comme des groupoïdes relevait du folklore mathématique. Cependant cela a été mis noir sur blanc pour la première fois, de manière sémantique, par et Thomas Streicher dans un article en 1998 intitulé « The groupoid interpretation of type theory », dans lequel ils montraient que la théorie des types intensifs avait un modèle dans la catégorie des groupoïdes. Il s'agissait du premier modèle véritablement « homotopique » de la théorie des types, bien qu'il ne s'agisse que d'un modèle « 1-dimensionnel » (les modèles traditionnels dans la catégorie des ensembles étant homotopiquement de dimension zéro).
Leur article annonçait également plusieurs développements ultérieurs de la théorie homotopique des types. Par exemple, ils ont noté que le modèle groupoïde répond à une règle appelée , qui n'est autre que la restriction à l'axiome d'univalence proposée par Vladimir Voïevodski dix ans plus tard (l'axiome pour les 1-types est toutefois beaucoup plus simple à formuler, puisqu'une notion de cohérence de l'« équivalence » n'est pas requise). Ils ont également défini les « catégories avec isomorphisme comme égalité » et ont émis la conjecture que, dans un modèle utilisant des groupoïdes de dimension supérieure, on aurait pour de telles catégories la propriété que . Cela a été prouvé plus tard par Benedikt Ahrens, Krzysztof Kapulkin et Michael Shulman..
Histoire ancienne : catégories des modèles et groupoïdes supérieurs Steve Awodey et son élève Michael Warren, en 2005, ont construit les premiers modèles de théorie intenstionnelle des types à dimensions supérieures à l'aide de catégories de modèles de Quillen. Ces résultats ont été présentés pour la première fois en public lors de la conférence FMCS 2006Foundational Methods in Computer Science, University of Calgary, June 7th - 9th, 2006 au cours de laquelle Warren a donné une conférence intitulée Modèles homotopiques de la théorie intentionnelle des types, qui lui a également servi de résumé de thèse (les membres du comité de thèse présents étaient Awodey, Nicola Gambino et Alex Simpson). Un résumé est contenu dans le résumé de la thèse de WarrenMichael Warren, Homotopy Models of Intensional Type Theory..
En 2006, lors d'un atelier sur les types identité organisé à l'université d'UppsalaIdentity Types - Topological and Categorical Structure, Workshop, Uppsala, November 13-14, 2006, deux exposés ont été consacrés à la relation entre la théorie intentionnelle des types et les systèmes de factorisation: l'un de Richard Garner, Systèmes de factorisation pour la théorie des typesRichard Garner, Factorisation axioms for type theory., et l'autre de Michael Warren, Catégories de modèles et types identité intensifs. Des idées similaires furent apportées dans les exposés de Steve Awodey, Théorie des types des catégories de dimension supérieure, et de Thomas Streicher, Types identité par opposition aux oméga-groupoïdes faibles : quelques idées, certains problèmes. Lors de la même conférence, Benno van den Berg a présenté Les types comme oméga-catégories faibles. Au cours de cette présentation, il a exposé les idées qui ont ensuite fait l'objet d'un document commun avec Richard Garner.
Les toutes premières constructions de modèles de dimensions supérieures traitaient le problème de cohérence typique des modèles de théorie des types dépendants, et diverses solutions ont été développées. Un exemple a été donné en 2009 par Voevodsky et un autre en 2010 par van den Berg et Garner. En 2014, une solution générale, s'appuyant sur la construction de Voevodsky, a finalement été proposée par Lumsdaine et Warren..
En 2007, lors du PSSL 86Il s'agit de la édition du Peripatetic Seminar on Sheaves and Logic (séminaire péripatéticien sur les faisceaux et la logique), cf. ., Awodey a présenté un exposé intitulé Théorie homotopique des types (il s'agissait du premier usage public de ce terme, qui a été inventé par AwodeyPreliminary list of PSSL86 participants. ). Awodey et Warren ont résumé leurs résultats dans l'article intitulé Homotopy theoretic models of identity types, publié sur le serveur de préimpression ArXiv en 2007. et publié en 2009. Une version plus détaillée est apparue dans la thèse de Warren intitulée Homotopy theoretic aspects of constructive type theory en 2008.
À peu près au même moment, Vladimir Voevodsky enquêtait de manière indépendante sur la théorie des types dans le contexte de la recherche d'une langue pour la formalisation pratique des mathématiques. En , il a posté Une très brève note sur le lambda-calcul homotopique. sur la liste de diffusion Types, qui esquissait les contours d'une théorie des types avec des produits dépendants, des sommes et des univers et d'un modèle de cette théorie ensembles simpliciaux de Kan. Il a commencé par dire et termine par . Il faisait référence aux problèmes complexes de cohérence qui n'ont pas été résolus avant 2009. Cette note incluait une définition syntaxique des types égalité' supposés être interprétés dans le modèle par des espaces de chemins, mais ne tenait pas compte des règles de Per Martin-Löf relatives aux types identité. Il a également stratifié les univers par dimension homotopique en plus de la taille, une idée qui a ensuite été en grande partie rejetée.
Sur le plan syntaxique, Benno van den Berg a supposé en 2006 que la tour des types identité d'un type, en théorie intentionnelle des types, devrait avoir la structure d'une ω-catégorie, voire d'un ω-groupoïde, au sens globulaire algébrique de Michael Batanin. Ceci a ensuite été prouvé de manière indépendante par van den Berg et Garner dans l'étude Types are weak omega-groupoids (publié en 2008). et par Peter Lumsdaine dans l'article Weak ω-Categories from Intensional Type Theory (publié en 2009) et dans le cadre de la thèse de son doctorat en 2010 Higher Categories from Type Theories..
L'axiome d'univalence, la théorie synthétique de l'homotopie et les types inductifs supérieurs Le concept d'une fibration univalente a été introduit par Voevodsky au début de 2006Notes on homotopy lambda calculus, mars 2006. Cependant, en raison de l'insistance de toutes les présentations de la théorie des types de Martin-Löf sur la propriété que les types identité, dans le contexte vide, ne peuvent contenir uniquement que de la réflexivité, Voevodsky n'a pas reconnu jusqu'en 2009 que ces types identité pouvaient être utilisés en combinaison avec les univers univalents. En particulier, l'idée selon laquelle l'univalence peut être introduite simplement en ajoutant un axiome à la théorie de type de Martin-Löf existante n'est apparue qu'en 2009.
Également en 2009, Voevodsky a élaboré davantage de détails d'un modèle de théorie des types dans les complexes de Kan et a observé que l'existence d'une fibration de Kan universelle pourrait être utilisée pour résoudre les problèmes de cohérence des modèles de catégories de la théorie des types. Il a également prouvé, à l'aide d'une idée d'AK Bousfield, que cette fibration universelle était univalente : la fibration associée d'équivalences homotopiques par paires entre les fibres est équivalente à la fibration chemins-espace de la base.
Pour formuler l'univalence en tant qu'axiome, Voevodsky a trouvé un moyen de définir des équivalences syntaxiquement qui possèdent la propriété importante que le type représentant la déclaration « f est une équivalence » était (sous l'hypothèse de l'extension de fonction) (-1)-tronqué (cf. contractile si habité). Cela lui a permis de donner une déclaration syntaxique de l'univalence, généralisant l'extensionalité de Hofmann et Streicher à des dimensions supérieures. Il a également pu utiliser ces définitions d'équivalence et de contractibilité pour commencer à développer des quantités significatives de dans l'assistant de preuves Rocq. Ceci a formé la base de la bibliothèque appelée plus tard Fondations et finalement UniMathGitHub repository, Univalent Mathematics..
L'unification des différents fils de fer a débuté en par une réunion informelle à l'Université Carnegie-Mellon, au cours de laquelle Voevodsky a présenté son modèle dans les complexes de Kan et son code Rocq à un groupe comprenant Awodey, Warren, Lumsdaine et Robert Harper, Dan Licata, Michael Shulman, et d'autres. Cette réunion a produit les grandes lignes d'une preuve (de Warren, Lumsdaine, Licata et Shulman) selon laquelle toute équivalence d'homotopie est une équivalence (au sens cohérent de Voevodsky), basée sur l'idée de la théorie des catégories visant à améliorer les équivalences en équivalences équivalentes. Peu de temps après, Voevodsky prouva que l'axiome d'univalence impliquait l'extensionalité de la fonction.