Théorie homotopique des types

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

À 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 », 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 0-dimensionnels).

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 « extensionnalité de l'univers », 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 « l'équivalence est l'égalité ». 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 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 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.

En 2006, lors d'un atelier sur les types identité organisé à l'Université d'Uppsala, 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, 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 PSSL86, 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 Awodey ). 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 septembre 2006, 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 « 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) 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.

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 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 « 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.

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. Dans le cadre d'un didacticiel Coq pour cet atelier, Andrej Bauer a écrit une petite bibliothèque Coq 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 (le premier commit de cette dernière 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), 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 théorie homotopique des types 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.

Fondations univalentes

L'expression « fondations univalentes » convient pour tous d'être étroitement liée à la théorie homotopique des types, mais tout le monde ne l'utilise pas de la même manière. Vladimir Voevodsky l'avait utilisé, à l'origine, pour faire référence à sa vision d'un système fondamental des mathématiques dans lequel les objets de base étaient des types homotopiques, reposant sur une théorie des types satisfaisant l'axiome d'univalence et formalisée dans un assistant de preuve informatique.

À mesure que les travaux de Voevodsky s'intégraient à la communauté d'autres chercheurs travaillant sur la théorie homotopique des types, les fondations univalentes étaient parfois utilisés indifféremment avec la « théorie homotopique des types » et, d'autres fois, pour se référer uniquement à son utilisation en tant que système fondateur (excluant, par exemple, l'étude de la sémantique modèle-catégorique ou de la métathéorie du calcul). Par exemple, le sujet de l'année spéciale (IAS) a été officiellement qualifié de « fondations univalentes », même si une grande partie du travail effectué dans ce domaine portait sur la sémantique et la métathéorie en plus des fondations. Le livre produit par les participants au programme IAS était intitulé Théorie homotopique des types : Fondations univalentes des mathématiques ; bien que cela puisse faire référence à l'une ou l'autre utilisation, puisque le livre ne traite que de la théorie homotopique des types comme fondement mathématique.

Année Spéciale sur les Fondations Univalentes des Mathématiques

Une animation montrant le développement du livre Homotopy Type Theory sur le site GitHub par les participants à le projet de l'année spéciale sur les fondations univalentes

En 2012 et en 2013, des chercheurs de l'Institut d'études avancées ont organisé « Une Année Spéciale sur les Fondations Univalentes des Mathématiques ». L'année spéciale a rassemblé des chercheurs en topologie, en informatique, en théorie des catégories et en logique mathématique. Le programme était organisé par Steve Awodey, Thierry Coquand et Vladimir Voïevodski.

Pendant le programme, Peter Aczel, qui était l'un des participants, a mis en place un groupe de travail qui a étudié la manière de faire la théorie des types de manière informelle mais rigoureuse, dans un style analogue à celui des mathématiciens ordinaires. Après des expériences initiales, il est apparu clairement que cela était non seulement possible, mais également très bénéfique, et qu'un livre (le livre Homotopy Type Theory) pourrait et devrait être écrit. De nombreux autres participants au projet ont ensuite rejoint l'effort avec un support technique, l'écriture, la correction des preuves et l'apport d'idées. Fait inhabituel pour un texte mathématique, il a été développé en collaboration et à l'air libre sur GitHub. Il est publié sous une licence Creative Commons qui permet aux utilisateurs de créer leur propre version du livre.

Plus généralement, l'année spéciale a été un catalyseur pour le développement de l'ensemble du sujet. Le livre Homotopy Type Theory n'était que le plus visible des résultats. ACM Computing Reviews a classé le livre parmi les publications remarquables de 2013 dans la catégorie informatique théorique.

Concepts clés

Théorie des types intensive	Théorie de l'homotopie
les types $A$	les espaces $A$
termes $a$	points $a$
$a:A$	$a\in A$
type dépendant $x:A\ \vdash \ B(x)\$	fibration $B\to A$
Type d'identité $\mathrm {Id} _{A}(a,b)$	espace de chemin
$p:\mathrm {Id} _{A}(a,b)$	chemin $p:a\to b$
$\alpha :\mathrm {Id} _{\mathrm {Id} _{A}(a,b)}(p,q)$	homotopie $\alpha :p\Rightarrow q$

Propositions en tant que types

La théorie homotopique des types 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 homotopique des types, 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.

Égalité

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

Plus important encore, étant donné un chemin $p:a=b$ et une preuve de propriété $P(a)$, la preuve peut être " transportée " le long du chemin $p$ pour donner une preuve de la propriété $P(b)$. (De manière équivalente, un objet de type $P(a)$ peut être transformé en un objet de type $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 homotopique des types et les mathématiques classiques entre en jeu. En mathématiques classiques, une fois que l'égalité de deux valeurs $a$ et $b$ a été établi, $a$ et $b$ peuvent être utilisés indifféremment par la suite, sans distinction entre elles. Cependant, dans la théorie homotopique des types, il peut y avoir plusieurs chemins différents $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 homotopique des types, 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 $a$, l'espace des chemins $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 $a=b$ pour $\mathrm {Id} _{A}(a,b)$, laissant ainsi le type $A$ de $a,b$ implicite, à ne pas confondre avec $\mathrm {id} _{A}:A\to A$, désignant la fonction identité sur $A$.

Équivalence de types

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

$f:A\to B$

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

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

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

c'est-à-dire

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

$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 $A\rightarrow A$ et $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 $A$ et $B$ :

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

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

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

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

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

Les fonctions de type

$A\to B$

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

$A\simeq B$.

L'axiome d'univalence

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

$(A=B)\to (A\simeq B),$

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

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

$(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 .

Applications

Preuve de théorème

La théorie homotopique des types 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.

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.

La théorie homotopique des types 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 homotopique des types, cela signifie que les deux formes qui représentent les valeurs des symboles sont topologiquement équivalentes.

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.

Programmation informatique

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 homotopique des types.

La théorie des types cubiques est une tentative de donner du contenu informatique à la théorie homotopique des types.

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 homotopique des types.

Voir également

Bibliographie

• 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.

Articles connexes

• Calcul des constructions
• Correspondance Curry-Howard

Liens externes

• Site officiel
• (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