| Title:
|
Type theoretical approaches to opetopes (English) |
| Author:
|
Curien, Pierre-Louis |
| Author:
|
Ho Thanh, Cédric |
| Author:
|
Mimram, Samuel |
| Language:
|
English |
| Journal:
|
Higher Structures |
| ISSN:
|
2209-0606 |
| Volume:
|
6 |
| Issue:
|
1 |
| Year:
|
2022 |
| Pages:
|
80-181 |
| Summary lang:
|
English |
| . |
| Category:
|
math |
| . |
| Summary:
|
Opetopes are algebraic descriptions of shapes corresponding to compositions in higher dimensions. As such, they offer an approach to higher-dimensional algebraic structures, and in particular, to the definition of weak $\omega$-categories, which was the original motivation for their introduction by Baez and Dolan. They are classically defined inductively (as free operads in Leinster’s approach, or as zoom complexes in the formalism of Kock et al.), using abstract constructions making them difficult to manipulate with a computer. In this paper, we present two purely syntactic descriptions of opetopes as sequent calculi, the first using variables to implement the compositional nature of opetopes, the second using a calculus of higher addresses. We prove that well-typed sequents in both systems are in bijection with opetopes as defined in the more traditional approaches. Additionally, we propose three variants to describe opetopic sets. We expect that the resulting structures can serve as natural foundations for mechanized tools based on opetopes. (English) |
| Keyword:
|
Opetope |
| Keyword:
|
Opetopic set |
| Keyword:
|
Type theory |
| Keyword:
|
Polynomial functor |
| MSC:
|
03B15 |
| MSC:
|
18D50 |
| idZBL:
|
Zbl 1494.18017 |
| idMR:
|
MR4456593 |
| DOI:
|
10.21136/HS.2022.02 |
| . |
| Date available:
|
2026-03-13T09:55:40Z |
| Last updated:
|
2026-03-13 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/153446 |
| . |
| Reference:
|
[1] Baez, John C., Dolan, James: Higher-dimensional algebra. III. n-categories and the algebra of opetopes.Advances in Mathematics, Vol. 135, Iss. 2, 145-206, DOI:10.1006/aima.1997.1695 10.1006/aima.1997.1695 |
| Reference:
|
[2] Bar, Krzysztof, Kissinger, Aleks, Vicary, Jamie: Globular: an online proof assistant for higher-dimensional rewriting.arXiv e-prints, arXiv:1612.01093 MR 3751039 |
| Reference:
|
[3] Cheng, Eugenia: The category of opetopes and the category of opetopic sets.Theory and Applications of Categories, Vol. 11, No. 16, 353-374 MR 2005691, 10.70930/tac/v8omllae |
| Reference:
|
[4] Finster, Eric: Opetopic.net.http://opetopic.net, http://opetopic.net |
| Reference:
|
[5] Finster, Eric, Mimram, Samuel: A Type-Theoretical Definition of Weak \omega-Categories.In 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:
|
[6] Gabriel, Peter, Ulmer, Friedrich: Lokal präsentierbare Kategorien.Lecture notes in mathematics, vol. 221, Springer-Verlag, Berlin-New York |
| Reference:
|
[7] Gambino, Nicola, Kock, Joachim: Polynomial functors and polynomial monads.Mathematical Proceedings of the Cambridge Philosophical Society, Vol. 154, Iss. 1, 153-192, DOI:10.1017/S0305004112000394 MR 3002590, 10.1017/S0305004112000394 |
| Reference:
|
[8] Gepner, David, Haugseng, Rune, Kock, Joachim: \infty-Operads as Analytic Monads.International Mathematics Research Notices, https://doi.org/10.1093/imrn/rnaa332, DOI:10.1093/imrn/rnaa332 MR 4466007, 10.1093/imrn/rnaa332 |
| Reference:
|
[9] Harnik, Victor, Makkai, Michael, Zawadowski, Marek: Computads and multitopic sets.arXiv:0811.3215 [math.CT] |
| Reference:
|
[10] Hermida, Claudio, Makkai, Michael, Power, John: On weak higher dimensional categories. I. 1.Journal of Pure and Applied Algebra, Vol. 154, Iss. 1-3, 221-246, DOI:10.1016/S0022-4049(99)00179-6 10.1016/S0022-4049(99)00179-6 |
| Reference:
|
[11] Hermida, Claudio, Makkai, Michael, Power, John: On weak higher-dimensional categories. I. 3.Journal of Pure and Applied Algebra, Vol. 166, Iss. 1-2, 83-104, DOI:10.1016/S0022-4049(01)00014-7 MR 1868540, 10.1016/S0022-4049(01)00014-7 |
| Reference:
|
[12] Ho Thanh, Cédric: The equivalence between opetopic sets and many-to-one polygraphs.arXiv:1806.08645 [math.CT] |
| Reference:
|
[13] Ho Thanh, Cédric: Opetopy.https://github.com/altaris/opetopy, https://github.com/altaris/opetopy |
| Reference:
|
[14] Hofmann, Martin: Syntax and semantics of dependent types.Semantics and logics of computation (Cambridge, 1995), pages 79-130, Publ. Newton inst. 14 |
| Reference:
|
[15] Kock, Joachim: Polynomial functors and trees.International Mathematics Research Notices, Vol. 2011, Iss. 3, 609-673, DOI:10.1093/imrn/rnq068 MR 2764874, 10.1093/imrn/rnq068 |
| Reference:
|
[16] Kock, Joachim, Joyal, André, Batanin, Michael, Mascari, Jean-François: Polynomial functors and opetopes.Advances in Mathematics, Vol. 224, Iss. 6, 2690-2737, DOI:10.1016/j.aim.2010.02.012 MR 2652220, 10.1016/j.aim.2010.02.012 |
| Reference:
|
[17] Lack, Stephen, Power, John: Gabriel-Ulmer duality and Lawvere theories enriched over a general base.Journal of Functional Programming, Vol. 19, Iss. 3-4, 265-286, DOI:10.1017/S0956796809007254 MR 2541349, 10.1017/S0956796809007254 |
| Reference:
|
[18] Leinster, Tom: Higher operads, higher categories.Cambridge University Press, DOI:10.1017/cbo9780511525896 10.1017/cbo9780511525896 |
| Reference:
|
[19] Loday, Jean-Louis, Vallette, Bruno: Algebraic operads.Springer Science & Business Media, Volume 346 MR 2954392 |
| Reference:
|
[20] Makkai, Michael: First order logic with dependent sorts, with applications to category theory.Available at https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf |
| . |
