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