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 France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

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

Plan 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.