Skip to Main content Skip to Navigation

A type theoretic approach to weak w-categories and related higher structures

Abstract : We study a type theoretic definition of weak omega-categories originally introduced by Finster and Mimram, inspired both from ideas coming from homotopy type theory and from a definition of weak omega-category due to Grothendieck and Maltsiniotis. The advantages of such an approach are multiple: The language of type theory allows for a definition restricted to only a few rules, it also provides an explicit syntax on which one can perform inductive reasoning, and gives an algorithm for implementing a proof-assistant dedicated to exploring weak omega-categories. The work we present about this type theory is organized along two main axes: We investigate the theoretical grounds for this definition and relate it to an other known definition of weak omega-categories, and we present the proof-assistant based on this theory together with practical considerations to improve its use. We also consider a generalization of this approach to other related higher structures.We start with an introduction to the language of dependent type theory that we rely on to introduce our definitions, presenting both the syntax and the semantics that we study by means of categorical tools. We then present weak omega-categories and a type theory that defines them. We detail the categorical semantics of this theory and our main contribution in this direction establishes an equivalence between its models and the prior definition of weak omega-categories due to Grothendieck and Maltsiniotis. This definition has enabled us to implement a proof-assistant capable of checking whether a given morphism is well-defined in the theory of weak omega-category, and we present this implementation together with a few examples demonstrating both the capabilities of such a tool, and its tediousness in the vanilla version. To improve this issue, we present two main additional features allowing to partially automating its use: The suspension and the functorialization. These two operations are defined by similar techniques of induction on the syntax of the type theory. We then generalize this definition of weak omega-categories and present a type theoretic framework that is both modular enough to allow for defining higher structures, and constrained enough to precisely understand its semantics. This enables us to sketch a connection with the theory of monads with arities. Using this framework, we introduce and study two other definitions of higher structures: Monoidal weak omega-categories and cubical weak omega-categories. By using syntactic reasoning we are able to defines translations back and forth between the type theory defining weak omega-categories and the one describing monoidal weak omega-categories. One of our main result is to show that these translations imply an equivalence at the level of models: It shows that the monoidal omega-categories are equivalent to the omega-categories with a single object thus justifying the correctness of the appellation monoidal. We then give an alternate presentation of the type theory defining monoidal weak omega-categories, which diverges from our framework but is more standalone, and prove it to be equivalent to the previous presentation. We finally introduce in our framework a definition of cubical weak omega-categories and study its semantics, our main result along these lines is to characterize the models of this type theory and extract a mathematical definition equivalent to them.
Complete list of metadatas
Contributor : Abes Star :  Contact
Submitted on : Monday, January 11, 2021 - 4:14:07 PM
Last modification on : Tuesday, January 12, 2021 - 3:32:45 AM


Version validated by the jury (STAR)


  • HAL Id : tel-03106197, version 1



Thibaut Benjamin. A type theoretic approach to weak w-categories and related higher structures. Formal Languages and Automata Theory [cs.FL]. Institut Polytechnique de Paris, 2020. English. ⟨NNT : 2020IPPAX077⟩. ⟨tel-03106197⟩



Record views


Files downloads