Théorie des types homotopiques

À une époque, l’idée que les types de la théorie des types intensive, avec leurs types identité, pouvaient être considérés comme des groupoïdes relevait du folklore mathématique. Elle a été précisée pour la première fois, de manière sémantique, dans l’article paru en 1998 de Martin Hofmann et Thomas Streicher, intitulé « The groupoid interpretation of type theory[2] », dans lequel ils montraient que la théorie des types intensifs avait un modèle dans la catégorie des groupoïdes[3]. 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 0-dimensionnels).

Leur article annonçait également plusieurs développements ultérieurs de la théorie des types homotopiques. Par exemple, ils ont noté que le modèle groupoïde répond à une règle appelée « extensionnalité de l’univers », qui n’est autre que la restriction à l’axiome d’univalence proposée par Vladimir Voevodsky 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 « l’équivalence est l’égalité ». Cela a été prouvé plus tard par Benedikt Ahrens, Krzysztof Kapulkin et Michael Shulman[4].

Steve Awodey et son élève Michael Warren, en 2005, ont construit les premiers modèles de théorie des types intensive à 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 2006[5] au cours de laquelle Warren a donné une conférence intitulée " Modèles homotopiques de la théorie des types d'intensive ", 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 Warren[6].

En 2006, lors d’un atelier sur les types identité organisé à l’Université d’Uppsala[7], deux exposés ont été consacrés à la relation entre la théorie des types intensive et les systèmes de factorisation: l’un de Richard Garner, "Systèmes de factorisation pour la théorie des types"[8], 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[9].

En 2007, lors du PSSL86[10] Awodey a présenté un exposé intitulé "Théorie des types homotopiques" (il s'agissait du premier usage public de ce terme, qui a été inventé par Awodey[11] ). 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[12] 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 septembre 2006, il a posté " Une très brève note sur le lambda-calcul homotopique "[13] 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 "Le λ-calcul homotopique est un système de types hypothétique (pour le moment)" et termine par "Pour le moment, une grande partie de ce que j'ai dit ci-dessus se situe au niveau des conjectures. Même la définition du modèle de TS dans la catégorie homotopique n’est pas triviale ". 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 des types intensive, 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)[14] et par Peter Lumsdaine dans l'étude " 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 "[15].

Le concept d'une fibration univalente a été introduit par Voevodsky au début de 2006[16]. 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 de 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 " théorie synthétique de l'homotopie " dans l'assistant de preuves Coq. Ceci a formé la base de la bibliothèque appelée plus tard " Fondations " et finalement " UniMath "[17].

L'unification des différents fils de fer a débuté en février 2010 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 Coq à 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.

Le prochain événement essentiel était un mini-atelier organisé par Steve Awodey, Richard Garner, Per Martin-Löf et Vladimir Voevodsky, à l' Institut de recherche mathématique d'Oberwolfach, intitulé " L'interprétation homotopique de la théorie des types constructive "[18]. Dans le cadre d'un didacticiel Coq pour cet atelier, Andrej Bauer a écrit une petite bibliothèque Coq[19] basée sur les idées de Voevodsky (mais n'utilisant en réalité aucun de ses codes). Cela devint finalement le noyau de la première version de la bibliothèque "HoTT" Coq[20] (le premier commit de cette dernière[21] de Michael Shulman indique " Développement basé sur les fichiers d'Andrej Bauer, avec de nombreuses idées extraites des fichiers de Vladimir Voevodsky ") L’une des choses les plus importantes qui ont émergé de la réunion d’Oberwolfach était l’idée de base des types inductifs supérieurs, due à Lumsdaine, Shulman, Bauer et Warren. Les participants ont également formulé une liste de questions ouvertes importantes, notamment pour savoir si l'axiome d'univalence satisfait à la canonicité (toujours ouverte, bien que certains cas particuliers aient été résolus de manière positive[22] - [23]), si l'axiome d'univalence comporte des modèles non standard (depuis il y eut une réponse positive de Shulman), et comment définir des types (semi)simpliciaux (encore ouverte dans MLTT, bien que cela puisse être fait dans le système de types hotomotopiques (HTS) de Voevodsky, une théorie des types à deux types d’égalité).

Peu de temps après l'atelier Oberwolfach, le site Web et le blog[24] théorie des types homotopiques ont été créés et le sujet a commencé à être popularisé sous ce nom. L’historique du blog donne une idée des progrès importants réalisés au cours de cette période[25].

La théorie des types homotopiques utilise une version modifiée de l'interprétation " propositions en tant que types " de la théorie des types, selon laquelle les types peuvent également représenter des propositions. Les termes peuvent alors représenter des preuves. Cependant, dans la théorie des types homotopiques, contrairement aux " propositions en tant que types " standard, un rôle particulier est joué par les " simples propositions " qui sont grosso modo celles qui ont au plus un terme, jusqu'à l'égalité propositionnelle. Celles-ci s'apparentent davantage à des propositions logiques conventionnelles que des types généraux, c'est en ce sens qu'elles sont non probantes.

Le concept fondamental de la théorie des types homotopiques est le chemin. Dans cette théorie, le type ${\displaystyle a=b}$ est le type de tous les chemins du point ${\displaystyle a}$ jusqu'au point ${\displaystyle b}$.(Par conséquent, une preuve qu'un point ${\displaystyle a}$ est égal à un point ${\displaystyle b}$ est la même chose qu'un chemin du point ${\displaystyle a}$ jusqu'au point ${\displaystyle b}$) Pour tout point ${\displaystyle a}$, il existe un chemin de type ${\displaystyle a=a}$, correspondant à la propriété de la réflexivité de l'égalité. Un chemin de type ${\displaystyle a=b}$ peut être inversé, formant un chemin de type ${\displaystyle b=a}$, correspondant à la propriété de la symétrie de l’égalité. Deux chemins de type ${\displaystyle a=b}$ et ${\displaystyle b=c}$ peuvent être concaténés, formant un chemin de type ${\displaystyle a=c}$. Ceci correspond à la propriété de la transitivité de l'égalité.

Plus important encore, étant donné un chemin ${\displaystyle p:a=b}$ et une preuve de propriété ${\displaystyle P(a)}$, la preuve peut être " transportée " le long du chemin ${\displaystyle p}$ pour donner une preuve de la propriété ${\displaystyle P(b)}$. (De manière équivalente, un objet de type ${\displaystyle P(a)}$ peut être transformé en un objet de type ${\displaystyle P(b)}$) Ceci correspond à la propriété de substitution de l'égalité. Ici, une différence importante entre les mathématiques de la théorie des types homotopiques et les mathématiques classiques entre en jeu. En mathématiques classiques, une fois que l'égalité de deux valeurs ${\displaystyle a}$ et ${\displaystyle b}$ a été établi, ${\displaystyle a}$ et ${\displaystyle b}$ peuvent être utilisés indifféremment par la suite, sans distinction entre elles. Cependant, dans la théorie des types homotopiques, il peut y avoir plusieurs chemins différents ${\displaystyle a=b}$, et transporter un objet le long de deux chemins différents donnera deux résultats différents. Par conséquent, dans la théorie des types homotopiques, lors de l'application de la propriété de substitution, il est nécessaire d'indiquer quel chemin est utilisé.

En général, une "proposition" peut avoir plusieurs preuves différentes. (Par exemple, le type de tous les nombres naturels, considéré comme une proposition, a tous les nombres naturels comme preuve) Même si une proposition n'a qu'une preuve ${\displaystyle a}$, l'espace des chemins ${\displaystyle a=a}$ peut être non-trivial en quelque sorte. Une "simple proposition" est tout type qui est vide ou ne contient qu'un seul point avec un espace de chemins trivial.

A noter que les gens écrivent ${\displaystyle a=b}$ pour ${\displaystyle \mathrm {Id} _{A}(a,b)}$, laissant ainsi le type ${\displaystyle A}$ de ${\displaystyle a,b}$ implicite, à ne pas confondre avec ${\displaystyle \mathrm {id} _{A}:A\to A}$, désignant la fonction identité sur ${\displaystyle A}$.

Deux types ${\displaystyle A}$ et ${\displaystyle B}$ appartenant à un univers ${\displaystyle {\cal {U}}}$ sont définis comme équivalents s’il existe une équivalence entre eux. Une équivalence est une fonction

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

qui a à la fois un inverse gauche et un inverse droit, en ce sens que pour ${\displaystyle g}$ et ${\displaystyle h}$ convenablement choisis, les types suivants sont tous deux habités :

${\displaystyle \mathrm {Id} _{B\rightarrow B}(f\circ g,\mathrm {id} _{B}),}$

${\displaystyle \mathrm {Id} _{A\rightarrow A}(h\circ f,\mathrm {id} _{A}).}$

c'est-à-dire

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

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

Ceci exprime une notion générale de "f a à la fois un inverse gauche et un inverse droit", en utilisant des types égalité. À noter que les conditions d'inversibilité ci-dessus sont des types égalité dans les types de fonction ${\displaystyle A\rightarrow A}$ et ${\displaystyle B\rightarrow B}$. On suppose généralement l’axiome d’extensionalité des fonctions, ce qui garantit leur équivalence aux types suivants qui expriment l’inversibilité en utilisant l’égalité sur le domaine et le codomaine ${\displaystyle A}$ et ${\displaystyle B}$ :

${\displaystyle \prod _{y:B}\ \mathrm {Id} _{B}((f\circ g)(y),\mathrm {id} _{B}(y)),}$

${\displaystyle \prod _{x:A}\ \mathrm {Id} _{A}((h\circ f)(x),\mathrm {id} _{A}(x)).}$

c'est-à-dire pour tous ${\displaystyle x:A}$ et ${\displaystyle y:B}$,

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

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

Les fonctions de type

${\displaystyle A\to B}$

avec une preuve qu'elles sont des équivalences sont notées par

${\displaystyle A\simeq B}$.

Ayant défini des fonctions équivalentes comme ci-dessus, on peut montrer qu’il existe un moyen canonique de transformer les chemins en équivalences. En d'autres termes, il existe une fonction du type

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

qui exprime que les types ${\displaystyle A,B}$ qui sont égaux sont, en particulier, également équivalents.

L' axiome d'univalence affirme que cette fonction est elle-même une équivalence[27]. ^:115 Par conséquent, nous avons

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

"En d'autres termes, l'identité est équivalente à l'équivalence. En particulier, on peut dire que «les types équivalents sont identiques». " [27] ^:4

La théorie des types homotopiques permet de traduire les preuves mathématiques dans un langage de programmation destiné aux assistants de preuve informatique beaucoup plus facilement qu'auparavant. Cette approche offre aux ordinateurs la possibilité de vérifier des preuves difficiles[35].

L'un des objectifs des mathématiques est de formuler des axiomes à partir desquels pratiquement tous les théorèmes mathématiques peuvent être dérivés et démontrés sans ambiguïté. Les preuves correctes en mathématiques doivent suivre les règles de la logique. Ils doivent pouvoir être dérivés sans erreur d’axiomes et d’énoncés déjà prouvés[35].

La théorie des types homotopiques ajoute l'axiome d'univalence, qui relie l'égalité des propositions logico-mathématiques à la théorie de l'homotopie. Une équation telle que «a = b» est une proposition mathématique dans laquelle deux symboles différents ont la même valeur. Dans la théorie des types homotopiques, cela signifie que les deux formes qui représentent les valeurs des symboles sont topologiquement équivalentes[35].

Selon Giovanni Felder, directeur de l'Institut d'études théoriques à l'ETH Zürich, ces relations d'équivalences topologiques peuvent être mieux formulées dans la théorie de l'homotopie, car elles sont plus complètes: la théorie de l'homotopie explique non seulement pourquoi «a est égal à b», mais également comment le calculer. En théorie des ensembles, il faudrait en plus définir cette information, ce qui rend plus difficile la traduction de propositions mathématiques dans des langages de programmation[35].

Dès 2015, d'intenses travaux de recherche étaient en cours pour modéliser et analyser formellement le comportement informatique de l'axiome d'univalence dans la théorie des types homotopiques[36].

La théorie des types cubiques est une tentative de donner du contenu informatique à la théorie des types homotopiques[37].

Cependant, on pense que certains objets, tels que les types semi-simpliciaux, ne peuvent être construits sans référence à une notion d'égalité exacte. Par conséquent, diverses théories de types à deux niveaux ont été développées. Elles répartissent leurs types en types fibrants respectant les chemins et en types non-fibrants. La théorie des types cubiques cartésienne est la première théorie des types à deux niveaux qui donne une interprétation informatique complète de la théorie des types homotopiques[38].

• The Univalent Foundations Program, Homotopy Type Theory : Univalent Foundations of Mathematics, Princeton, NJ, Institute for Advanced Study, 2013 (MR 3204653, lire en ligne) (GitHub version cited in this article.)
• Awodey et Warren, « Homotopy theoretic models of identity types », Mathematical Proceedings of the Cambridge Philosophical Society, vol. 146, n^o 1,‎ janvier 2009, p. 45–55 (DOI 10.1017/S0305004108001783, Bibcode 2008MPCPS.146...45A, arXiv 0709.0248) As PDF.
• Steve Awodey, Epistemology versus Ontology, Springer, coll. « Logic, Epistemology, and the Unity of Science », 2012, 183–201 p. (ISBN 978-94-007-4434-9, DOI 10.1007/978-94-007-4435-6_9), « Type theory and homotopy »
• Awodey, « Structuralism, Invariance, and Univalence », Philosophia Mathematica, vol. 22, n^o 1,‎ 2014, p. 1–11 (DOI 10.1093/philmat/nkt030, lire en ligne, consulté le 21 février 2015)
• Martin Hofmann et Thomas Streicher, Twenty Five Years of Constructive Type Theory, Clarendon Press, 1998, 83–112 p. (ISBN 978-0-19-158903-4), « The groupoid interpretation of type theory » As postscript.

• Calcul des constructions
• Correspondance Curry-Howard

• (en) Homotopy Type Theory
• Homotopy type theory wiki
• Vladimir Voevodsky's webpage on the Univalent Foundations
• Homotopy Type Theory and the Univalent Foundations of Mathematics par Steve Awodey
• "Constructive Type Theory and Homotopy" – Cours vidéo par Steve Awodey at the Institute for Advanced Study