Fondements univalents

Les principales idées des fondements univalents ont été formulées par Vladimir Voevodsky en 2006/2009. La seule référence de connexion philosophique entre les fondements univalents et les idées antérieures apparait dans les conférences Bernays de Voevodsky en 2014[3]. Le terme "univalence" a été choisi par Voevodsky[4]. 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 Coq et Agda. La première bibliothèque appelée "Foundations" a été créé par Vladimir Voevodsky en 2010[5]. Maintenant "Foundations" est une partie d'un outil plus important conçu par plusieurs auteurs et appelé UniMath[6]. La bibliothèque "Foundations" a également inspiré d'autres bibliothèques de mathématiques formalisées, telles que les bibliothèques HoTT Coq[7] et HoTT Agda[8], 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 juin 2014.

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 papier visionnaire FOLDS[9]. 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 Voevodsky 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 de 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)[10].

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 Bauer[11]. 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[12].

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égories[13].

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.

Un compte rendu de la construction par Voevodsky 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 Voevodsky[14]. Des modèles univalents à valeurs dans les catégories des diagrammes inverses des ensembles simpliciaux ont été construits par Michael Shulman[15]. 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 Voevodsky 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 Huber[16] 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[17].

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:

1. définir les types semi-simpliciaux, les H-types ou les (infini, 1)-catégories sur les types
2. ajouter au calcul des constructions inductives un système de gestion de l'univers qui permettrait d'implémenter les règles de redimensionnement.
3. développer une variante constructive de l'axiome d'univalence[18].

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.

• Théorie des types homotopiques

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Univalent foundations » (voir la liste des auteurs).

• Michael Makkai, First Order Logic with Dependent Sorts, with Applications to Category Theory, 1995
• Vladimir Voevodskyi, Paul Bernays lectures, 2014

• wikt:univalent

Bibliothèques de mathématiques formelles

• Foundations library (2010-current)
• HoTT library (2011-current)