Title: Towards a syntax for higher dimensional categories

 

 

Time: 10:00 am, April 19th (Thursday), 2018

 

Venue: Lecture room (Room 334), Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

 

Opetopes, originally introduced by Baez and Dolan, are geometric shapes describing the structure of compositions in all dimensions. As such, they offer an approach to higher category theory, and in particular, to the definition of weak omega-categories. They are classically defined inductively (e.g., as free operads in Leinster's approach, or as zoom complexes in the formalism of Batanin et al.), using abstract constructions which render them difficult to manipulate with a computer. Here we present a purely syntactic description of opetopes, using a calculus of addresses, first as a raw system (which accepts non well-formed objects), which we then control through a typing system (which accepts only opetopes). Our main result is that these well-typed syntactic opetopes are (up to recursive reordering of addresses) in bijection with opetopes as defined in the more traditional approaches. We take profit of this syntactic presentation to give a simple definition of the category of opetopes by generators and relations. We expect that the resulting structures can serve as natural foundations to mechanized tools based on opetopes.