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

 

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

Bio: Pierre-Louis Curien is a CNRS Senior Researcher. He got his PhD in Computer Science from University Paris 7 in 1979. He was successively a member of the LITP laboratory at Paris 7 University (1981-1986) and of the LIENS laboratory at ENS (1987-1998), before creating the laboratory PPS (Proofs, Programs and Ssytems) at Paris 7 University, of which he was the director until 2009. He won the IBM France Computer Science award in 1990. He has been the member of several scientifc councils (University Paris 7, INSII Institute of CNRS, City of Paris). He is currently member of the scientific council of CIRM (International Center for Mathematical Encounters, Marseille). He is head ot the joint Inria Paris Diderot CNRS team pi_r2. His research acitivities spread over the semantics of programming languages, proof theory, category theory, and more recently homotopical algebra. He is editor in chief of the journal Mathematical Structures in Computer Science. He co-organised the first thematic semester fostering Computer Science at the prestigious Institut Poincaré in 2014 (on the semantics of proofs and programs). He is the author of around 60 research papers and has directed more than 20 PhD theses.