HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

A type-theoretical definition of weak ω-categories

Abstract : 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.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

Contributor : Samuel Mimram Connect in order to contact the contributor
Submitted on : Thursday, June 13, 2019 - 10:03:12 AM
Last modification on : Wednesday, April 27, 2022 - 3:48:02 AM


Files produced by the author(s)



Eric Finster, Samuel Mimram. A type-theoretical definition of weak ω-categories. LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1-12, ⟨10.1109/LICS.2017.8005124⟩. ⟨hal-02154846⟩



Record views


Files downloads