Colloque – Formalisation des mathématiques et types dépendants – Denis-Charles Cisinski : La logique des catégories supérieures

Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-2025Colloque - Formalisation des mathématiques et types dépendants - Denis-Charles Cisinski : La logique des catégories supérieuresDenis-Charles CisinskiProfesseur, Universität RegensburgRésuméLa logique des catégories supérieures (ou encore des ∞-catégories) est une variation de la théorie des types qui est homotopique par nature et dans laquelle la notion de catégorie est le concept primitif – celui que l'on ne définit jamais ! Une généralisation adéquate de l'axiome d'univalence de Voevodsky fait de cette théorie un langage très expressif, et ce, assez pour qu'il puisse produire ses propres interprétations sémantiques. Cela fournit un système de fondation des mathématiques au cœur duquel les concepts de la théorie des catégories ainsi que de la théorie de l'homotopie sont implémentés. Une logique des logiques. Une interprétation sémantique de cette logique est produite en mathématiques classiques par la théorie des ∞-catégories telle que développée par Joyal et Lurie. Une formulation en théorie des types dépendants, via la théorie de Riehl-Shulman, est l'objet d'un projet en cours de Buchholtz et Weinberger. Cette logique permet de formuler constructivement bien des théories considérées comme avancées (e.g. cohomologie étale des schémas dérivés ou non, catégories dérivées des faisceaux quasi cohérents) d'une manière proche de la pratique. C'est aussi une nouvelle manière d'appréhender la logique elle-même, de sorte que la distance entre syntaxe et sémantique est en apparence très significativement réduite : les logiques sont les termes d'un type, i.e. les objets d'une ∞-catégorie.Denis-Charles CisinskiDenis-Charles Cisinski est professeur de mathématiques à l'Universität Regensburg, en Allemagne. Il a occupé des postes permanents à l'université de Toulouse et à l'université Sorbonne-Paris-Nord, et est un ancien membre de l'Institut universitaire de France. Ses recherches portent sur l'algèbre homotopique, la théorie des catégories, la K-théorie et la cohomologie des schémas. Il est l'auteur de trois monographies : Les préfaisceaux comme modèles des types d'homotopie (2007), Triangulated categories of mixed motives (2019), et Higher categories and homotopical algebra (2019).