Rencontre, 15 mars 2018

Programme

10:30 – 12:00

Marcelo Fiore (University of Cambridge, UK)

Invited talk: An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures

The starting point of the talk will be the identification of structure common to tree-like combinatorial objects, exemplifying the situation with abstract syntax trees (as used in formal languages) and with opetopes (as used in higher-dimensional algebra). The emerging mathematical structure will be then formalized in a categorical setting, unifying the algebraic aspects of the theory of abstract syntax and the theory of opetopes. This realization conceptually allows one to transport viewpoints between these, now bridged, mathematical theories and I will explore it here in the direction of higher-dimensional algebra, giving an algebraic combinatorial framework for a generalisation of the slice construction for generating opetopes. The technical work will involve setting up a microcosm principle for near-semirings and subsequently exploit it in the cartesian closed bicategory of generalised species of structures. Connections to (cartesian and symmetric monoidal) equational theories, type theory, lambda calculus, and algebraic combinatorics will be mentioned in passing.

14:00 – 15:00

Bérénice Delcroix-Oger (IRIF, Univ. Paris Diderot)

Invited talk: Why operads can be seen as enhanced species and what they are used for.

Species have been introduced by Joyal in the 80s and are defined as functors (usually from the category of finite sets and bijections to itself), endowed with some operations. An operad can then be seen as a species enhanced with a natural transformation. After an explanation, with examples, of these definitions, I will give some examples illustrating the power of these notions, especially concerning freeness of algebras.

15:30 – 16:30

Samuel Mimram (École Polytechnique)

Invited talk: Mechanized tools for higher categories

Weak higher categories generalize the traditional notion of category by comprising higher-dimensional cells and using those in order to provide witnesses for structural axioms. Due to their very general nature, they are difficult to manipulate and even to define. In this talk, we will present two recently developed (theoretical and software) tools in order to assist the mathematician working with those structures. Firstly, we will describe a type theory whose models are precisely the globular categories, thus providing a proof assistant in order to ensure the validity of coherence laws in those categories. Secondly, we will generalize higher-dimensional rewriting techniques to Gray categories (a semi-strict variant of tricategories) in order to obtain coherence results for algebraic structures in low dimensional weak categories.