A Sequent Calculus for Opetopes

Cédric Ho Thanh (1, 2) , Pierre-Louis Curien (1, 2) , Samuel Mimram (3, 2)

1 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
2 PI.R2 - Design, study and implementation of languages for proofs and programs
3 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]

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 ω-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. Here, we present a purely syntactic description of opetopes and opetopic sets as a sequent calculus. Our main result is that well-typed opetopes in our sense are in bijection with opetopes as defined in the more traditional approaches. We expect that the resulting structures can serve as natural foundations for mechanized tools based on opetopes.

Mots clés: Opetope; Polynomial functor; Type theory; Opetopic set

Domaines: Topologie algébrique [math.AT]; Catégories et ensembles [math.CT]; Informatique [cs]

Cédric Ho Thanh, Pierre-Louis Curien, Samuel Mimram. A Sequent Calculus for Opetopes. LICS 2019 - Logic in computer science 2019, Jun 2019, Vancouver, Canada. ⟨hal-02406569⟩