07 – Théorie des types dépendants et formalisation des mathématiques : Espaces d’Eilenberg-MacLane et cohomologie

Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202507 - Théorie des types dépendants et formalisation des mathématiques : Espaces d'Eilenberg-MacLane et cohomologiePlan du cours :opération de débouclage des groupes ;un exemple paradigmatique de définition de types qui ne sont pas des ensembles, les espaces d'Eilenberg-MacLane ;utilisation de ces types pour définir les groupes de cohomologie.