Parmi les fondements des mathématiques, les fondements univalents sont une approche des fondements des mathématiques constructivesVoir plus bas la discussion sur la relation entre mathématiques classiques et constructives dans les fondements univalents. qui part de l'idée que les mathématiques étudient des structures de types univalents qui correspondent, en projection sur la théorie des ensembles, aux types d'homotopie. Les fondements univalents sont inspirés à la fois par les idées platoniciennes de Hermann Grassmann et Georg Cantor et par la théorie des catégories d'Alexandre Grothendieck. Ils s'écartent de la logique des prédicats comme système sous-jacent de la déduction formelle et la remplacent par une version de la théorie des types de Per Martin-Löf. Le développement des fondements univalents est étroitement lié au développement de la théorie homotopique des types.
Les fondements univalents sont compatibles avec le structuralisme dans la mesure où une notion de structure mathématique appropriée (c'est-à-dire catégorique) est adoptée..
Historique Les principales idées des fondements univalents ont été formulées par Vladimir Voïevodski en 2006-2009. La seule référence de connexion philosophique entre les fondements univalents et les idées antérieures apparaît dans les conférences Bernays de Voïevodski en 2014. Le terme univalence a été choisi par Voïevodskiunivalence axiom in nLab. Une discussion plus détaillée de l'histoire de certaines des idées qui contribuent à l'état actuel des fondements univalents peut être consultée à la page sur la théorie des types homotopiques.
Les fondements univalents, lorsqu'ils sont combinés avec la théorie des types de Martin-Löf, constituent un système pratique de formalisation des mathématiques modernes. Une quantité considérable de mathématiques a été formalisée à l'aide de ce système et d'assistants de preuve comme Rocq et Agda. La première bibliothèque appelée Foundations a été créée par Vladimir Voïevodski en 2010Foundations library, see https://github.com/vladimirias/Foundations. Maintenant Foundations est une partie d'un outil plus important conçu par plusieurs auteurs, appelé UniMathUniMath library, see https://github.com/UniMath/UniMath. La bibliothèque Foundations a également inspiré d'autres bibliothèques de mathématiques formalisées, telles que les bibliothèques HoTT CoqHoTT Coq library, see https://github.com/HoTT/HoTT et HoTT AgdaHoTT Agda library, see https://github.com/HoTT/HoTT-Agda, qui ont poussé les idées des fondements univalents dans de nouvelles directions.
Une étape importante pour les fondements univalents a été la conférence de Thierry Coquand au séminaire Bourbaki de .
Principes Les fondements univalents sont issus de tentatives de fonder les mathématiques sur la théorie des catégories supérieures. La tentative la plus proche des fondements univalents repose sur les idées que Michael Makkai a exposées dans son article visionnaire FOLDSMakkai (1995). La principale différence entre les fondements univalents et les fondations proposées par Makkai tient à ce que les « analogues aux ensembles de dimension supérieure » correspondent à des groupoïdes infinis et à ce que les catégories devraient être considérées comme des analogues de dimension supérieure aux ensembles partiellement ordonnés .
À l'origine, les fondements univalents ont été développés par Vladimir Voïevodski dans le but de permettre à ceux qui travaillent dans le domaine des mathématiques pures classiques d'utiliser des ordinateurs pour vérifier leurs théorèmes et constructions. Le fait que les nouveaux fondements soient intrinsèquement constructifs a été découvert pendant l'écriture de la bibliothèque Foundations (qui fait maintenant partie d'UniMath). À l'heure actuelle, dans les fondements univalents, les mathématiques classiques sont considérées comme une rétractation des mathématiques constructives en ce sens que les mathématiques classiques sont à la fois un sous-ensemble des mathématiques constructives faites de théorèmes et constructions basées sur le principe du tiers exclu et aussi un « quotient » des mathématiques constructives par la relation d'équivalence modulo l'axiome du tiers exclu.
Dans le système de formalisation des fondements univalents qui repose sur la théorie des types de Martin-Löf et ses descendants tels que le calcul des constructions inductives, les analogues de dimension supérieure aux ensembles sont représentés par des types. Le monde des types est stratifié par le concept de h-level (homotopy level)See of Pelayo-Warren (2014).
Les types de h-level 0 sont ceux qui sont égaux au type « point ». Ils sont aussi appelés types contractiles.
Les types de h-level 1 sont ceux pour lesquels deux éléments quelconques sont égaux. De tels types sont appelés « propositions » dans les fondements univalents. La définition des propositions en termes de h-level est conforme à la définition suggérée auparavant par Awodey and BauerAwodey-Bauer (2001). De sorte que, alors que toutes les propositions sont des types, tous les types ne sont pas des propositions. Être une proposition est une propriété d'un type qui nécessite d'être prouvée. Par exemple, la première construction fondamentale des fondements univalents s'appelle iscontr. C'est une fonction de types vers types. Si X est un type alors iscontr X est un type qui a un objet si et seulement si X est contractile. C'est un théorème (qui s'appelle isapropiscontr dans la bibliothèque UniMath) que pour tout X le type iscontr X est de h-level 1; en conséquence, être un type contractile est une propriété. Cette distinction entre propriétés qui sont observées par des objets de types h-level 1 et structures qui sont observées par des objets de type h-levels supérieurs est très importante dans les fondements univalents.
Les types de h-level 2 s'appellent des ensembles. Le fait que le type des entiers naturels est de h-level 2 est un théorème (isasetnat dans UniMath). Les créateurs des fondements univalents prétendent que la formalisation univalente des ensembles dans la théorie des types de Martin-Löf est le meilleur environnement disponible aujourd'hui pour le raisonnement formel sur tous les aspects des mathématiques ensemblistes, quelle que soit l'approche constructive ou classique.
Les Catégories sont définies comme des types de h-level 3 (voir la bibliothèque RezkCompletion d'UniMath) avec une structure supplémentaire qui est très similaire à la structure sur les types de h-level 2 qui définit les ensembles partiellement ordonnés. La théorie des catégories dans les fondements univalents est à la fois différente et plus riche que la théorie des catégories dans le monde ensembliste avec une nouvelle distinction entre les pré-catégories et les catégoriesSee Benedikt Ahrens, Chris Kapulkin, Michael Shulman, Univalent categories and the Rezk completion, https://arxiv.org/abs/1303.0584.
Un tutoriel de Thierry Coquand (part 1, part 2) expose les principales idées des fondements univalents et leur rapport avec les mathématiques constructives. L'article d'Alvaro Pelayo et Michael Warren les présente du point de vue des mathématiques classiques. Voir aussi cet article au sujet de la bibliothèque Foundations.
Développements actuels Un compte rendu de la construction par Voïevodski d'un modèle univalent de la théorie des types de Martin-Löf avec des valeurs dans les ensembles simpliciaux de Kan a été publié par Chris Kapulkin, Peter LeFanu Lumsdaine et Vladimir VoïevodskiChris Kapulkin, Peter LeFanu Lumsdaine and Vladimir Voevodsky, "The Simplicial Model of Univalent Foundations", see https://arxiv.org/abs/1211.2851. Des modèles univalents à valeurs dans les catégories des diagrammes inverses des ensembles simpliciaux ont été construits par Michael ShulmanMichael Shulman "Univalence for inverse diagrams and homotopy canonicity", https://arxiv.org/abs/1203.3253. Ces modèles ont montré que l'axiome d'univalence est indépendant de l'axiome du tiers exclu pour les propositions.
Le modèle de Voïevodski est non constructif puisqu'il utilise de façon substantielle l'axiome du choix.
Le problème de trouver un moyen constructif d'interpréter les règles de la théorie des types de Martin-Löf qui de plus satisfasse à l'axiome d'univalence et à la canonicité pour les entiers naturels reste ouvert. Une solution partielle est esquissée dans un papier de Marc Bezem, Thierry Coquand et Simon HuberM. Bezem, T. Coquand and S. Huber, "A model of type theory in cubical sets", see http://www.cse.chalmers.se/~coquand/mod1.pdf dans lequel reste une difficulté majeure qui concerne la propriété calculatoire de l'éliminateur pour les types identité. Les idées de ce papier sont maintenant poussées dans diverses directions dont la théorie des types cubiques.
Nouvelles tendances La plupart des travaux de formalisation des mathématiques dans le cadre des fondements univalents sont faits en utilisant divers sous-systèmes et extensions du Calcul des constructions inductives.
Il y a cependant trois problèmes classiques dont la solution, malgré de nombreuses tentatives, n'a pas pu être construite en utilisant le calcul des constructions inductives: définir les types semi-simpliciaux, les H-types ou les (infini, 1)-catégories sur les types ajouter au calcul des constructions inductives un système de gestion de l'univers qui permettrait d'implémenter les règles de redimensionnement. développer une variante constructive de l'axiome d'univalenceV. Voevodsky, Univalent Foundations Project (a modified version of an NSF grant application), . Ces problèmes non résolus montrent que, si le calcul des constructions inductives est un bon outil pour commencer le développement des fondements univalents, l'utilisation d'assistants de preuve informatisés pour ses aspects les plus sophistiqués nécessitera une nouvelle génération de systèmes de déduction formelle et de calcul.
Voir aussi Théorie homotopique des types
Références
Bibliographie Michael Makkai, First Order Logic with Dependent Sorts, with Applications to Category Theory, 1995
Liens externes wikt:univalent Bibliothèques de mathématiques formelles Foundations library (2010-current) HoTT library (2011-current)
Catégorie:Fondements des mathématiques Catégorie:Théorie des types