SMF

Exposé Bourbaki 1085 : Théorie des types dépendants et axiome d'univalence

Exposé Bourbaki 1085 : Dependent type theory and axiom of univalence

Thierry COQUAND
Exposé Bourbaki 1085 : Théorie des types dépendants et axiome d'univalence
  • Consulter un extrait
  •  
                
  • Année : 2015
  • Tome : 367-368
  • Format : Électronique
  • Langue de l'ouvrage :
    Français
  • Class. Math. : 03B15, 18A15.
  • Pages : 367-386
  • DOI : 10.24033/ast.951

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.

Dependent type theory aims at being a foundation of mathematics different from set theory. Motivated by an interpretation of a type as a homotopy type (a space “up to homotopy”) V. Voevodsky has introduced a stratification of types following the complexity of their equality. The notion of type appears in this way to be a generalization of the notion of set. This interpretation also suggests and validates the axiom of univalence, which is a strong form of the axiom of extensionality. We present some consequences of this axiom, in particular what it entails for the formal representation of the notion of category in type theory.

Théorie des types, axiome d'univalence, $\infty $-groupoïdes.
Type theory, axiom of univalence, $\infty $-groupoids.

Électronique
Electronic
Prix public Public price 10.00 €
Prix membre Member price 7.00 €
Quantité
Quantity
- +