Accueil > Actualités > Séminaire Thierry Coquand : Théorie homotopique des types et en particulier ses travaux autour de la théorie cubique des types

Séminaire Thierry Coquand : Théorie homotopique des types et en particulier ses travaux autour de la théorie cubique des types

Jeudi 24 novembre, 14h30-15h30, salle 105@LINA, séminaire de Thierry Coquand (Göteborg University).

Présentation des travaux en théorie homotopique des types, en particulier autour de la théorie cubique des types

Résumé

Les travaux de Voevodsky suggèrent une extension de la théorie des types dependents qui résout certains problèmes de modularité (égalité extensionelle et quotients). La justification de cette extension est développée en utilisant le tiers-exclu et l’axiome du choix. Nous présentons un modèle de cette extension dans un cadre constructif, et
qui peut s’écrire avec avantage directement comme une théorie des types. Cette théorie vérifie la propriété que tout terme clos de type entier se réduit sur un entier en forme canonique. Nous pouvons aussi donner une sémantique de l’opération de "troncation propositionnelle” dans ce cadre.
On utilise une variation des ensembles simpliciaux (ensembles cubiques) et cette sémantique donne une structure de modèle (au sens de Quillen) sur ces ensembles cubiques de manière effective (travaux de Christian Sattler). Il n’est pas clair si une telle description effective est possible dans un cadre simplicial.
Une question naturelle est si l’on peut utiliser un tel modèle pour établir des résultats d’indépendance (par exemple, de l’axiome du choix dénombrable), et nous discuterons quelques réponses partielles.


Dernière modification : vendredi 2 novembre 2018