| Title:
|
Globular weak $\omega$-categories as models of a type theory (English) |
| Author:
|
Benjamin, Thibaut |
| Author:
|
Finster, Eric |
| Author:
|
Mimram, Samuel |
| Language:
|
English |
| Journal:
|
Higher Structures |
| ISSN:
|
2209-0606 |
| Volume:
|
8 |
| Issue:
|
2 |
| Year:
|
2024 |
| Pages:
|
1-69 |
| Summary lang:
|
English |
| . |
| Category:
|
math |
| . |
| 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. (English) |
| Keyword:
|
weak category |
| Keyword:
|
type theory |
| Keyword:
|
coherator |
| Keyword:
|
initiality conjecture |
| MSC:
|
03B15 |
| MSC:
|
18D99 |
| idZBL:
|
Zbl 1558.18005 |
| idMR:
|
MR4835386 |
| DOI:
|
10.21136/HS.2024.07 |
| . |
| Date available:
|
2026-03-13T14:32:02Z |
| Last updated:
|
2026-03-13 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/153472 |
| . |
| Reference:
|
[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 |
| Reference:
|
[2] Ara, Dimitri: Sur les ∞-groupoïdes de Grothendieck et une variante ∞-catégorique.PhD thesis, Université Paris 7 |
| Reference:
|
[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 10.1006/aima.1998.1724 |
| Reference:
|
[4] Benjamin, Thibaut: A type theoretic approach to weak ω-categories and related higher structures.PhD thesis, Institut Polytechnique de Paris |
| Reference:
|
[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 MR 4481907, 10.4230/LIPIcs.TYPES.2021.2 |
| Reference:
|
[6] Benjamin, Thibaut: Monoidal weak omega-categories as models of a type theory.Mathematical Structures in Computer Science, 1-37, DOI:10.1017/S0960129522000172 MR 4651605, 10.1017/S0960129522000172 |
| Reference:
|
[7] Benjamin, Thibaut, Finster, Eric, Mimram, Samuel: The CaTT proof assistant.https://github.com/thibautbenjamin/catt |
| Reference:
|
[8] Berger, Clemens: A cellular nerve for higher categories.Advances in Mathematics, Vol. 169, Iss. 1, 118-175 MR 1916373, 10.1006/aima.2001.2056 |
| Reference:
|
[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 MR 2925893, 10.1016/j.jpaa.2012.02.039 |
| Reference:
|
[10] Bourke, John: Iterated algebraic injectivity and the faithfulness conjecture. Higher structures, 4 (2).arXiv preprint math/1811.09532 MR 4133167 |
| Reference:
|
[11] Brunerie, Guillaume: On the homotopy groups of spheres in homotopy type theory.arXiv preprint arXiv:1606.05916 |
| Reference:
|
[12] Burroni, Albert: Higher-dimensional word problems with applications to equational logic.Theoretical computer science, Vol. 115, Iss. 1, 43-62 10.1016/0304-3975(93)90054-W |
| Reference:
|
[13] Cartmell, John: Generalised algebraic theories and contextual categories.Annals of pure and applied logic, Vol. 32, 209-243 10.1016/0168-0072(86)90053-9 |
| Reference:
|
[14] Cheng, Eugenia, Lauda, Aaron: Higher-dimensional categories: An illustrated guide book.Preprint |
| Reference:
|
[15] Dybjer, Peter: Internal Type Theory.Types for proofs and programs. TYPES 1995, pp 120-134, DOI:10.1007/3-540-61780-9_66 10.1007/3-540-61780-9_66 |
| Reference:
|
[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 MR 3776950, 10.1109/LICS.2017.8005124 |
| Reference:
|
[17] Finster, Eric, Reutter, David, Vicary, Jamie: A type theory for strictly unital ∞-categories.arXiv preprint arXiv:2007.08307 MR 4537044 |
| Reference:
|
[18] Gabriel, Peter, Ulmer, Friedrich: Lokal präsentierbare kategorien.Springer-Verlag, Volume 221 MR 0327863 |
| Reference:
|
[19] Grothendieck, Alexander: Pursuing stacks.Unpublished manuscript |
| Reference:
|
[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 |
| Reference:
|
[21] Joyal, André: Disks, duality and θ-categories.Preprint |
| Reference:
|
[22] Joyal, André: Quasi-categories and kan complexes.Journal of Pure and Applied Algebra, Vol. 175, Iss. 1-3, 207-222 MR 1935979, 10.1016/S0022-4049(02)00135-4 |
| Reference:
|
[23] Kelly, Gregory Maxwell: Basic concepts of enriched category theory.CUP Archive, Volume 64 |
| Reference:
|
[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 MR 2628809, 10.1016/j.aim.2010.01.007 |
| Reference:
|
[25] Leinster, Tom: A survey of definitions of n-category.Theory and applications of Categories, Vol. 10, Iss. 1, 1-70 MR 1883478 |
| Reference:
|
[26] Leinster, Tom: Higher operads, higher categories.Cambridge University Press, Volume 298 MR 2094071 |
| Reference:
|
[27] Lumsdaine, Peter LeFanu: Weak ω-categories from intensional type theory.International conference on typed lambda calculi and applications, pp 172-187 MR 2550047 |
| Reference:
|
[28] Maltsiniotis, Georges: Grothendieck ∞-groupoids, and still another definition of ∞-categories.Preprint arXiv:1009.2331 |
| Reference:
|
[29] Riehl, Emily: Category theory in context.Courier Dover Publications MR 4727501 |
| Reference:
|
[30] Street, Ross: Limits indexed by category-valued 2-functors.Journal of Pure and Applied Algebra, Vol. 8, Iss. 2, 149-181 |
| Reference:
|
[31] Street, Ross: The algebra of oriented simplexes.Journal of Pure and Applied Algebra, Vol. 49, Iss. 3, 283-335 10.1016/0022-4049(87)90137-X |
| Reference:
|
[32] Streicher, Thomas: Contextual categories and categorical semantics of dependent types.Semantics of type theory, pages 43-111, |
| Reference:
|
[33] Subramaniam, Chaitanya Leena: From dependent type theory to higher algebraic structures.ArXiv:2110.02804 |
| Reference:
|
[34] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics.https://homotopytypetheory.org/book MR 3204653 |
| Reference:
|
[35] Van Den Berg, Benno, Garner, Richard: Types are weak ω-groupoids.Proceedings of the London Mathematical Society, Vol. 102, Iss. 2, 370-394 MR 2769118, 10.1112/plms/pdq026 |
| Reference:
|
[36] Voevodsky, Vladimir: A C-system defined by a universe category.Theory and Applications of Categories, Vol. 30, Iss. 37, 1181-1215 MR 3402489, 10.70930/tac/a8860iyd |
| . |
