Résumé
Que veut dire le signe « égal » dans un programme informatique ? dans un texte mathématique ? La première définition précise de l’égalité, attribuée à Leibniz, dit que x et y sont égaux si et seulement s’ils satisfont les mêmes propriétés : ∀P, P(x) ⇔ P(y). Cette définition est équivalente à d’autres définitions plus récentes, en logique du premier ordre ou en théorie des ensembles, ainsi qu’à la définition en théorie des types introduite par Martin-Löf en 1973. Celle-ci se présente comme un type x = A y des identités (preuves d’égalité) entre x : A et y : A, un constructeur qui est l’axiome de réflexivité, et un éliminateur qui est la loi de remplacement entre égaux.
L’égalité de Martin-Löf, ou sa reformulation comme un prédicat inductif en Coq, est parfaite pour raisonner sur les types de premier ordre comme les entiers mais pose quelques difficultés sur les types plus riches. En particulier, on ne peut pas démontrer que deux fonctions égales point à point sont égales, ni que deux identités entre x et y sont égales. Cela conduit beaucoup de développements en Coq à ajouter comme axiomes l’extensionalité des fonctions et l’unicité des identités.
Un nouveau point de vue sur l’égalité en théorie des types est fourni par la théorie de l’homotopie en topologie algébrique et son extension à l’ordre supérieur : la structure de ω-groupoïde. On peut interpréter les identités comme des chemins et les identités entre identités comme des homotopies entre chemins. Sur la base de cette inspiration homotopique et catégorique, Voevodsky, Avodey, Coquand et d’autres ont, à partir de 2005, développé la théorie homotopique des types (Homotopy Type Theory, HoTT), une variante de la théorie des types où l’égalité joue un rôle central. Ainsi, HoTT définit les propositions logiques comme les types où tous les éléments sont égaux entre eux, et les ensembles comme les types où l’égalité est une proposition. HoTT introduit également de nouveaux outils : la troncature propositionnelle, les types quotients, les types inductifs d’ordre supérieur, qui ouvrent des possibilités nouvelles tant en logique mathématique qu’en programmation typée.
