05 – Théorie des types dépendants et formalisation des mathématiques : Le mystère de l’égalité ; la notion de type comme généralisation de la notion d’ensemble

Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202505 - Théorie des types dépendants et formalisation des mathématiques : Le mystère de l'égalité ; la notion de type comme généralisation de la notion d'ensemblePlan du cours :comment représenter la notion d'égalité en théorie des types ; stratification de Voevodsky des types ; une définition uniforme de la notion d'équivalence ; principe d'univalence ; application à la notion d'égalité des structures mathématiques et comparaison avec la théorie des ensembles.