Article
Full entry |
PDF
(1.6 MB)
Feedback
PDF
(1.6 MB)
Feedback
Keywords:
Opetope; Opetopic set; Type theory; Polynomial functor
Opetope; Opetopic set; Type theory; Polynomial functor
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.
References:
[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 DOI 10.1006/aima.1997.1695
[2] Bar, Krzysztof, Kissinger, Aleks, Vicary, Jamie: Globular: an online proof assistant for higher-dimensional rewriting. arXiv e-prints, arXiv:1612.01093 MR 3751039
[3] Cheng, Eugenia: The category of opetopes and the category of opetopic sets. Theory and Applications of Categories, Vol. 11, No. 16, 353-374 DOI 10.70930/tac/v8omllae | MR 2005691
[4] Finster, Eric: Opetopic.net. http://opetopic.net, http://opetopic.net
[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 DOI 10.1109/LICS.2017.8005124 | MR 3776950
[6] Gabriel, Peter, Ulmer, Friedrich: Lokal präsentierbare Kategorien. Lecture notes in mathematics, vol. 221, Springer-Verlag, Berlin-New York
[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 DOI 10.1017/S0305004112000394 | MR 3002590
[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 DOI 10.1093/imrn/rnaa332 | MR 4466007
[9] Harnik, Victor, Makkai, Michael, Zawadowski, Marek: Computads and multitopic sets. arXiv:0811.3215 [math.CT]
[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 DOI 10.1016/S0022-4049(99)00179-6
[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 DOI 10.1016/S0022-4049(01)00014-7 | MR 1868540
[12] Ho Thanh, Cédric: The equivalence between opetopic sets and many-to-one polygraphs. arXiv:1806.08645 [math.CT]
[13] Ho Thanh, Cédric: Opetopy. https://github.com/altaris/opetopy, https://github.com/altaris/opetopy
[14] Hofmann, Martin: Syntax and semantics of dependent types. Semantics and logics of computation (Cambridge, 1995), pages 79-130, Publ. Newton inst. 14
[15] Kock, Joachim: Polynomial functors and trees. International Mathematics Research Notices, Vol. 2011, Iss. 3, 609-673, DOI:10.1093/imrn/rnq068 DOI 10.1093/imrn/rnq068 | MR 2764874
[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 DOI 10.1016/j.aim.2010.02.012 | MR 2652220
[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 DOI 10.1017/S0956796809007254 | MR 2541349
[18] Leinster, Tom: Higher operads, higher categories. Cambridge University Press, DOI:10.1017/cbo9780511525896 DOI 10.1017/cbo9780511525896
[19] Loday, Jean-Louis, Vallette, Bruno: Algebraic operads. Springer Science & Business Media, Volume 346 MR 2954392
[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
Search
Partner of
