Type Theory for (∞,∞)-Categories, and Decomposition Spaces

Abstract

Aquesta tesi està formada per dos capítols, un sobre CaTT, una teoria de tipus per a (∞, ∞)-categories, i un sobre espais de descomposició, en col·laboració amb Joachim Kock.

El primer capítol conté dues parts. La primera part parteix de l'observació que la dimensió d'una operació coincideix amb la del diagrama subjacent que s'està composant, mentre que la dimensió d'una coherència és estrictament més gran que la del diagrama subjacent. Basant-nos en aquesta observació, proposem un nou conjunt de normes per descriure una (∞, ∞)-categoria, en el que les "condicions de contorn de variables lliures" de les normes originals a CaTT són substituides per condicions de "contorn" dimensionals. Les noves normes tenen l'avantatge de ser més geomètriques. El resultat principal consisteix en què les noves normes i les originals són mutuament admisibles. Construint el resultat principal, s'han obtingut diversos resultats tècnics d'interès independent. Un d'ells és el fet que les variables lliures d'un "pasting context" formen per si mateixes un "pasting context".

A la segona part introduim i estudiem una noció purament sintàctica de cons laxos i (∞, ∞)-limits en computads finits a CaTT. Convenientment, els computads finits són precisament els contexts a CaTT. Definitm un con sobre un context com un context obtingut per inducció sobre la llista de variables del context subjacent. En el cas en què el context subjacent és globular donem una descripció explícita del con i conjecturem que una descripció anàloga és vàlida per a contexts generals. Fem servir el con per controlar els tipus dels "term constructors" pel con universal. La implementació de la propietat universal segueix una estructura similar. Partint d'un con com a contexte, un conjunt de normes d'extensió de contexts produeixen un context amb la forma de transfor entre cons, i.e. un morfisme d'ordre superior entre cons. Com en el cas dels cons, utilitzem aquest context com a plantilla per a controlar els tipus dels "term constructors" necessaris per a la propietat universal.

El segon capítol, sobre espais de descomposició, té relació amb un teorema de Bergner, Osorno, Ozornova, Rovelli i Scheimbauer, que estableix una equivalència entre espais 2-Segal i certs espais double Segal augmentats, i també amb l'obra de Carlier, que va introduir la noció de "bicomodule configuration". Establim equivalències més generals, involucrant aplicacions simplicials d'espais 2-Segal i "abacus bicomodule configurations", extenent els resultats de Carlier. L'equivalència BOORS es recupera del cas particular de l'aplicació identitat. Un dels ingredients principals és un anàlisi de la relació entre les nocions d'augment de BOORS i Carlier, considerades independents prèviament.

Esta tesis tiene dos capítulos, uno sobre CaTT, una teoría de tipos para (∞, ∞)-categorías, y otro sobre espacios de descomposición, que es un trabajo conjunto con Joachim Kock.

El primer capítulo contiene dos partes. La primera parte comienza con el hecho de que la dimensión de una operación es igual a la del diagrama de pegado subyacente que se está componiendo, mientras que la dimensión de una coherencia es estrictamente mayor que la del diagrama de pegado subyacente. Basándonos en esta observación, proponemos un nuevo conjunto de reglas que describen una (∞, ∞)-categoría, en las que las condiciones de lado de variable libre de las reglas originales en CaTT se reemplazan por una condición de lado de dimensión. Las nuevas reglas tienen la ventaja de ser más geométricas. El resultado principal es que las nuevas reglas y las reglas originales son mutuamente admisibles. Para llegar al resultado principal, se presentan varios resultados técnicos, que son de interés independiente. Un resultado clave establece que las variables libres de un término en un pasting context forman por sí mismas un pasting context.

En la segunda parte, introducimos y estudiamos una noción puramente sintáctica de conos laxos y (∞, ∞)-límites en computads finitos en CaTT. Convenientemente, los computads finitos son precisamente los contexts en CaTT. Definimos un cono sobre un context como un context, que se obtiene por inducción sobre la lista de variables del contexto subyacente. En el caso en que el context subyacente es globular, damos una descripción explícita del cono y conjeturamos que una descripción análoga sigue siendo válida también para contexts generales. Usamos el cono para controlar los tipos de los constructores de términos para el cono universal. La implementación de la propiedad universal sigue una línea de ideas similar. Comenzando con un cono como context, un conjunto de reglas de extensión de context produce un context con la forma de un transformador entre conos, es decir, un morfismo superior entre conos. Al igual que en el caso de los conos, usamos este context como plantilla para controlar los tipos del term constructor requerido para la propiedad universal.

El segundo capítulo sobre espacios de descomposición se relaciona con un teorema de Bergner, Osorno, Ozornova, Rovelli y Scheimbauer, que establece una equivalencia entre espacios 2-Segal y ciertos espacios dobles Segal estables aumentados, y el trabajo de Carlier, quien introdujo la noción de bicomodule configuration. Establecemos equivalencias más generales, que involucran mapas simpliciales de espacios 2-Segal y abacus bicomodule configurations, extendiendo los resultados de Carlier. La equivalencia BOORS se recupera del caso especial del mapa de identidad. Un ingrediente principal es un análisis de la relación entre las nociones de BOORS y Carlier de augmentación, hasta ahora consideradas no relacionadas.

This thesis has two chapters, one on CaTT, a type theory for (∞, ∞)-categories, and one on decomposition spaces, which is joint work with Joachim Kock.

The first chapter contains two parts. The first part begins with the fact that the dimension of an operation is equal to that of the underlying pasting diagram being composed, whereas the dimension of a coherence is strictly larger than that of the underlying pasting diagram. Based on this observation we propose a new set of rules describing an (∞, ∞)-category, in which the free-variable side conditions of the original rules in CaTT are replaced by a dimension side condition. The new rules have the advantage of being more geometric. The main result is then that the new rules and the original rules are mutually admissible. Building up to the main result are a number of technical results, which are of independent interest. A key result states that the free variables of a term in a pasting context form themselves a pasting context.

In the second part we introduce and study a purely syntactic notion of lax cones and (∞, ∞)-limits on finite computads in CaTT. Conveniently, finite computads are precisely the contexts in CaTT. We define a cone over a context to be a context, which is obtained by induction over the list of variables of the underlying context. In the case where the underlying context is globular we give an explicit description of the cone and conjecture that an analogous description continues to hold also for general contexts. We use the cone to control the types of the term constructors for the universal cone. The implementation of the universal property follows a similar line of ideas. Starting with a cone as a context, a set of context extension rules produce a context with the shape of a transfor between cones, i.e. a higher morphism between cones. As in the case of cones, we use this context as a template to control the types of the term constructor required for universal property.

The second chapter on decomposition spaces relates to a theorem of Bergner, Osorno, Ozornova, Rovelli, and Scheimbauer, which states an equivalence between 2-Segal spaces and certain augmented stable doubleSegal spaces, and the work of Carlier, who introduced the notion of bicomodule configuration. We establish more general equivalences, involving simplicial maps of 2-Segal spaces and abacus bicomodule configurations, extending results of Carlier. The BOORS equivalence is recovered from the special case of the identity map. One main ingredient is an analysis of the relationship between the BOORS and Carlier notions of augmentation, hitherto considered unrelated.