Théorie des types pour les oméga-catégories faibles
Thibaut Benjamin
LIX, École polytechnique, Palaiseau
http://www.lix.polytechnique.fr/~tbenjamin/
Date(s) : 13/02/2020 iCal
11h00 - 12h30
Les oméga-catégories faibles sont une généralisation des catégories dans lesquelle chaque catégorie possède non seulement des objets et des flèches, mais aussi des cellules de dimension supérieures, qui peuvent se composer. Les axiomes que satisfont ces compositions sont tous « faibles », c’est à dire qu’ils sont à des cellules de dimension près.
Une structure similaire apparaît naturellement en théorie homotopique des types, où les types sont équipés d’une structure d’oméga-groupoide faible, qui, avec l’hypothèse d’homotopie, modélise les types d’homotopie. Les oméga-catégories faibles sont une version dirigée de ces derniers, et il est attendu qu’elles modélisent les types d’homotopie dirigée. Dans cette exposé je vais présenter la théorie des oméga catégories faibles sous la forme d’une théorie des types dépendants (à la Cartmell). Je présenterai ensuite rapidement les arguments qui permettent d’étudier les modèles de cette théorie, et de montrer qu’ils sont effectivement équivalents aux définitions existentes d’oméga-catégories faibles. Cela donnera une interprétation naturelle de la syntaxe de la théorie, et je montrerai comment une telle formulation permet de d’explorer certains aspects des oméga-catégories faibles par des raisonnements purement syntaxiques.
Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)
Catégories
