| Popis: |
PhD Thesis, 155 pages, in English (with English and French introductions); The first part of this dissertation defines "dependently typed algebraic theories", which are a strict subclass of the generalised algebraic theories (GATs) of Cartmell. We characterise dependently typed algebraic theories as finitary monads on certain presheaf categories, generalising a well-known result due to Lawvere, B\'enabou and Linton for ordinary multisorted algebraic theories. We use this to recognise dependently typed algebraic theories for a number of classes of algebraic structures, such as small categories, n-categories, strict and weak omega-categories, planar coloured operads and opetopic sets. We then show that every locally finitely presentable category is the category of models of some dependently typed algebraic theory. Thus, with respect to their Set-models, these theories are just as expressive as GATs, essentially algebraic theories and finite limit sketches. However, dependently typed algebraic theories admit a good definition of homotopy-models in spaces, via a left Bousfield localisation of a global model structure on simplicial presheaves. Some cases, such as certain "idempotent opetopic theories", have a rigidification theorem relating homotopy-models and (strict) simplicial models. The second part of this dissertation concerns localisations of presentable $(\infty,1)$-categories. We give a definition of "pre-modulator", and show that every accessible orthogonal factorisation system on a presentable $(\infty,1)$-category can be generated from a pre-modulator by iterating a plus-construction resembling that of sheafification. We give definitions of "modulator" and "left-exact modulator", and prove that they correspond to those factorisation systems that are modalities and left-exact modalities respectively. Thus every left-exact localisation of an $\infty$-topos is obtained by iterating the plus-construction associated to a left-exact modulator.; Dans la première partie de cette thèse, nous proposons une définition de « théorie algébrique à types/sortes dépendants » 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 démontrons un théorème de classification pour les 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 nous concluons que chaque catégorie localement finiment présentable admet une description comme catégorie des modèles d'une théorie algébrique à sortes dépendantes. Nous proposons également les définitions des modèles homotopiques strictes et faibles d'une théorie algébrique à 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 proposons les définitions de « modulateur » et de « modulateur exact à gauche » et nous montrons des correspondances avec les modalités et les modalités exactes à gauche respectivement. |
