2021/06/08 by Thibaut Benjamin, Benjamin, Thibaut, Eric Finster +3
Mathematics · #Advanced Topics in Algebra #Algebraic structures and combinatorial models #Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2106.04475
openalex publication_date 2021/06/08 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
We study the dependent type theory CaTT, introduced by Finster and Mimram,\nwhich presents the theory of weak \ω-categories, following the idea that\ntype theories can be considered as presentations of generalized algebraic\ntheories. Our main contribution is a formal proof that the models of this type\ntheory correspond precisely to weak \ω-categories, as defined by\nMaltsiniotis, by generalizing a definition proposed by Grothendieck for weak\n\ω-groupoids: Those are defined as suitable presheaves over a\ncat-coherator, which is a category encoding structure expected to be found in\nan \ω-category. This comparison is established by proving the initiality\nconjecture for the type theory CaTT, in a way which suggests the possible\ngeneralization to a nerve theorem for a certain class of dependent type\ntheories\n