Article
Full entry |
PDF
(1.0 MB)
Feedback
PDF
(1.0 MB)
Feedback
Keywords:
weak category; type theory; coherator; initiality conjecture
weak category; type theory; coherator; initiality conjecture
Summary:
We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $\omega$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $\omega$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $\omega$-groupoids: those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $\omega$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories.
References:
[1] Altenkirch, Thorsten, Rypacek, Ondrej: A syntactical approach to weak omega-groupoids. Computer science logic (CSL’12) – 26th international workshop / 21st annual conference of the EACSL
[2] Ara, Dimitri: Sur les ∞-groupoïdes de Grothendieck et une variante ∞-catégorique. PhD thesis, Université Paris 7
[3] Batanin, Michael: Monoidal globular categories as a natural environment for the theory of weak n-categories. Advances in Mathematics, Vol. 136, Iss. 1, 39-103 DOI 10.1006/aima.1998.1724
[4] Benjamin, Thibaut: A type theoretic approach to weak ω-categories and related higher structures. PhD thesis, Institut Polytechnique de Paris
[5] Benjamin, Thibaut: Formalisation of Dependent Type Theory: The Example of CaTT. 27th international conference on types for proofs and programs (TYPES 2021), pp 2:1-2:21, DOI:10.4230/LIPIcs.TYPES.2021.2 DOI 10.4230/LIPIcs.TYPES.2021.2 | MR 4481907
[6] Benjamin, Thibaut: Monoidal weak omega-categories as models of a type theory. Mathematical Structures in Computer Science, 1-37, DOI:10.1017/S0960129522000172 DOI 10.1017/S0960129522000172 | MR 4651605
[7] Benjamin, Thibaut, Finster, Eric, Mimram, Samuel: The CaTT proof assistant. https://github.com/thibautbenjamin/catt
[8] Berger, Clemens: A cellular nerve for higher categories. Advances in Mathematics, Vol. 169, Iss. 1, 118-175 DOI 10.1006/aima.2001.2056 | MR 1916373
[9] Berger, Clemens, Mellies, Paul-André, Weber, Mark: Monads with arities and their associated theories. Journal of Pure and Applied Algebra, Vol. 216, Iss. 8-9, 2029-2048 DOI 10.1016/j.jpaa.2012.02.039 | MR 2925893
[10] Bourke, John: Iterated algebraic injectivity and the faithfulness conjecture. Higher structures, 4 (2). arXiv preprint math/1811.09532 MR 4133167
[11] Brunerie, Guillaume: On the homotopy groups of spheres in homotopy type theory. arXiv preprint arXiv:1606.05916
[12] Burroni, Albert: Higher-dimensional word problems with applications to equational logic. Theoretical computer science, Vol. 115, Iss. 1, 43-62 DOI 10.1016/0304-3975(93)90054-W
[13] Cartmell, John: Generalised algebraic theories and contextual categories. Annals of pure and applied logic, Vol. 32, 209-243 DOI 10.1016/0168-0072(86)90053-9
[14] Cheng, Eugenia, Lauda, Aaron: Higher-dimensional categories: An illustrated guide book. Preprint
[15] Dybjer, Peter: Internal Type Theory. Types for proofs and programs. TYPES 1995, pp 120-134, DOI:10.1007/3-540-61780-9_66 DOI 10.1007/3-540-61780-9_66
[16] Finster, Eric, Mimram, Samuel: A Type-Theoretical Definition of Weak ω-Categories. 2017 32nd annual ACM/IEEE symposium on logic in computer science (LICS), pp 1-12, DOI:10.1109/LICS.2017.8005124 DOI 10.1109/LICS.2017.8005124 | MR 3776950
[17] Finster, Eric, Reutter, David, Vicary, Jamie: A type theory for strictly unital ∞-categories. arXiv preprint arXiv:2007.08307 MR 4537044
[18] Gabriel, Peter, Ulmer, Friedrich: Lokal präsentierbare kategorien. Springer-Verlag, Volume 221 MR 0327863
[19] Grothendieck, Alexander: Pursuing stacks. Unpublished manuscript
[20] Henry, Simon: The language of a model category. Presentation given at the HoTT Electronic Seminar Talks, https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html
[21] Joyal, André: Disks, duality and θ-categories. Preprint
[22] Joyal, André: Quasi-categories and kan complexes. Journal of Pure and Applied Algebra, Vol. 175, Iss. 1-3, 207-222 DOI 10.1016/S0022-4049(02)00135-4 | MR 1935979
[23] Kelly, Gregory Maxwell: Basic concepts of enriched category theory. CUP Archive, Volume 64
[24] Lafont, Yves, Métayer, François, Worytkiewicz, Krzysztof: A folk model structure on omega-cat. Advances in Mathematics, Vol. 224, Iss. 3, 1183-1231 DOI 10.1016/j.aim.2010.01.007 | MR 2628809
[25] Leinster, Tom: A survey of definitions of n-category. Theory and applications of Categories, Vol. 10, Iss. 1, 1-70 MR 1883478
[26] Leinster, Tom: Higher operads, higher categories. Cambridge University Press, Volume 298 MR 2094071
[27] Lumsdaine, Peter LeFanu: Weak ω-categories from intensional type theory. International conference on typed lambda calculi and applications, pp 172-187 MR 2550047
[28] Maltsiniotis, Georges: Grothendieck ∞-groupoids, and still another definition of ∞-categories. Preprint arXiv:1009.2331
[29] Riehl, Emily: Category theory in context. Courier Dover Publications MR 4727501
[30] Street, Ross: Limits indexed by category-valued 2-functors. Journal of Pure and Applied Algebra, Vol. 8, Iss. 2, 149-181
[31] Street, Ross: The algebra of oriented simplexes. Journal of Pure and Applied Algebra, Vol. 49, Iss. 3, 283-335 DOI 10.1016/0022-4049(87)90137-X
[32] Streicher, Thomas: Contextual categories and categorical semantics of dependent types. Semantics of type theory, pages 43-111,
[33] Subramaniam, Chaitanya Leena: From dependent type theory to higher algebraic structures. ArXiv:2110.02804
[34] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics. https://homotopytypetheory.org/book MR 3204653
[35] Van Den Berg, Benno, Garner, Richard: Types are weak ω-groupoids. Proceedings of the London Mathematical Society, Vol. 102, Iss. 2, 370-394 DOI 10.1112/plms/pdq026 | MR 2769118
[36] Voevodsky, Vladimir: A C-system defined by a universe category. Theory and Applications of Categories, Vol. 30, Iss. 37, 1181-1215 DOI 10.70930/tac/a8860iyd | MR 3402489
Search
Partner of
