Syntactic approaches to opetopes

zbMATH Open1494.18017arXiv1903.05848MaRDI QIDQ5094693FDOQ5094693

Authors: Pierre-Louis Curien, Cédric Ho Thanh, Samuel Mimram 

Publication date: 4 August 2022

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1903.05848

Recommendations

• Polynomial functors and opetopes
• Weak \(n\)-categories: Comparing opetopic foundations.
• scientific article; zbMATH DE number 2028926
• Weak \(n\)-categories: Opetopic and multitopic foundations.
• The web monoid and opetopic sets
• scientific article; zbMATH DE number 1303768
• On the Penon method of weakening algebraic structures
• Higher-dimensional algebra. III: \(n\)-categories and the algebra of opetopes
• Opetopes and chain complexes
• scientific article

zbMATH Keywords

type theorypolynomial functoropetopeopetopic set

Mathematics Subject Classification ID

Operads (general) (18M60) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Cites Work

• Algebraic operads
• Lokal präsentierbare Kategorien. (Locally presentable categories)
• Polynomial functors and trees
• Title not available (Why is that?)
• Title not available (Why is that?)
• Higher-dimensional algebra. III: \(n\)-categories and the algebra of opetopes
• On weak higher dimensional categories. I: Part 1
• Title not available (Why is that?)
• Polynomial functors and opetopes
• Polynomial functors and polynomial monads
• Gabriel–Ulmer duality and Lawvere theories enriched over a general base
• A Type-Theoretical Definition of Weak {\omega}-Categories
• On weak higher-dimensional categories. I: Part 3

Cited In (7)

• Opetopes and chain complexes
• Weak omega-categories from intensional type theory
• Polynomial functors and opetopes
• Actads
• A sequent calculus for opetopes
• A combinatorial-topological shape category for polygraphs
• Weak ω-Categories from Intensional Type Theory

Uses Software

• Globular
• GitHub
• opetopy

This page was built for publication: Syntactic approaches to opetopes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5094693)