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 metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-02154846
Contributor : Samuel Mimram <>
Submitted on : Thursday, June 13, 2019 - 10:03:12 AM
Last modification on : Tuesday, June 18, 2019 - 2:09:36 PM

File

mimram_catt.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

47

Files downloads

354