From dependent type theory to higher algebraic structures

Théorie des types dépendants et algèbre de dimension supérieure Dans la première partie de cette thèse, nous donnons une définition de "théorie algébrique à sortes dépendantes" qui généralise les théories algébriques "ordinaires" de Lawvere-Bénabou. Les théories algébriques à sortes dépendantes, en notre sens, forment une sous-classe stricte des "théories algébriques généralisées" de Cartmell. Nous montrons un théorème de classification des théories algébriques à sortes dépendantes, et nous utilisons ce théorème pour montrer l'existence de plusieurs de ces théories --- parmi elles, les théories des petites catégories, des n-catégories, des omega-catégories strictes et faibles, des opérades planaires colorées, et des ensembles opétopiques. Nous étudions le cas opétopique en détail. Nous montrons également une équivalence de Morita entre les théories algébriques à sortes dépendantes et les "théories essentiellement algébriques", et concluons que chaque catégorie localement finiment présentable admet une description comme catégorie des modèles d'une théorie algébriques à sortes dépendantes. Nous donnons également une définition des modèles "homotopiques" strictes et faibles d'une théorie algébriques à sortes dépendantes, et nous montrons un théorème de rigidification dans un cas particulier. La deuxième partie de cette dissertation concerne les localisations refléctives accessibles des infini-catégories localement présentables. Nous donnons une définition de "pré-modulateur" et montrons une correspondance entre les pré-modulateurs et les systèmes de factorisations accessibles sur une infini-catégorie localement présentable. Nous montrons également que chaque tel système de factorisation est engendré à partir d'un pré-modulateur par itération transfinie d'une "construction plus". Nous donnons les définitions de "modulateur" et "modulateur exact à gauche" et montrons une correspondance avec les modalités et les modalités exactes à gauche respectivement.