A type-theoretical definition of weak ω-categories

• Published in: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Main Authors: Finster, Eric, Mimram, Samuel
• Other Authors: Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT), Laboratoire des Sciences du Numérique de Nantes (LS2N), Laboratoire d'informatique de l'École polytechnique Palaiseau (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2017
• Subjects: [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT]; Iceland
• Online Access: https://inria.hal.science/hal-02154846; https://inria.hal.science/hal-02154846/document; https://inria.hal.science/hal-02154846/file/mimram_catt.pdf; https://doi.org/10.1109/LICS.2017.8005124

International audience We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of ω-groupoids. In this setup, ω-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an ω-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.