Exposé Bourbaki 1085 : Théorie des types dépendants et axiome d'univalence
Exposé Bourbaki 1085 : Dependent type theory and axiom of univalence
Astérisque | Exposés Bourbaki | 2015
Français
Cet exposé sera une introduction à la théorie des types dépendants et à l'axiome d'univalence. Cette théorie est une alternative à la théorie des ensembles comme fondement des mathématiques. Guidé par une interprétation d'un type comme un espace topologique « à homotopie près » (type d'homotopie), V. Voevoedsky a introduit une stratification des types suivant la complexité de leur égalité, qui fait apparaître la théorie des types comme une généralisation de la théorie des ensembles. Il a aussi formulé l'axiome d'univalence qui est une forme très forte du principe d'extensionalité. On discutera en particulier de quelques conséquences de cet axiome pour la représentation formelle de la notion de catégorie.
Théorie des types, axiome d'univalence, $\infty $-groupoïdes.
Électronique
Prix public
10.00 €
Prix membre
7.00 €
Quantité