06 – Théorie des types dépendants et formalisation des mathématiques : Modèles de la théorie des types et du principe d’univalence

Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202506 - Théorie des types dépendants et formalisation des mathématiques : Modèles de la théorie des types et du principe d'univalencePlan du cours :modèle de Voevodsky des ensembles simpliciaux et caractère non effectif de ces modèles ;modèles effectifs avec ensembles cubiques ;application à une définition de structure de modèle la Quillen sur certains modèles de préfaisceaux ;définition constructive des types d'homotopie des espaces topologiques.