Syntactic approaches to opetopes

MaRDI QIDQ5094693zbMATH OpenFDO

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

Publication date 4 August 2022

Full work available at URL https://arxiv.org/abs/1903.05848, https://higher-structures.math.cas.cz/api/files/issues/Vol6Iss1/CurHoTMim

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)

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.

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 DE number 2125641

Cites work

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

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

Describes a project that uses

Uses Software

• opetopy
• GitHub
• Globular

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)