Ré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.
