Higher-Dimensional Rewriting and Applications

3rd edition of the workshop
September 8-9, 2017, Oxford, United Kingdom
Satellite workshop of FSCD 2017, co-located with the STRING workshop.


Rewriting consists in orienting equalities. This seemingly simple point of view has given rise to a rich theory, which was first developped in computer science for handling strings and terms, and was then extended over the recent years to many other settings (operads, monoidal categories, higher categories, etc.), allowing it to have applications in algebra, homotopy theory and physics. All these generalizations fit into the general scope of higher-dimensional rewriting theory, which has emerged as a unifying algebraic framework.

The aim of the workshop is to gather people interested in pushing further rewriting theory, using (higher) category theory as a common language. It is open to all topics concerning higher-dimensional generalizations and applications of rewriting theory, including

Invited Speakers


Friday, September 8th

9:00–9:30: Registration

9:30–10:30: invited talk by Paul-André Melliès, Fibrational effects in string diagrams

One longstanding ambition of logic and of programming language semantics is to follow the path of mathematical physics and to geometrize itself. In this line of thought, I will discuss here a discovery which recently emerged from the algebraic study of the local state monad. The guiding idea (inspired by the notion of fiber bundle) is that a contravariant presheaf on a category C should not be seen as a functor from Cop to Set, but as a section of the trivial fibration C×Set→C. This fibrational and dependent point of view on functorial semantics has many advantages. In particular, it enables one to glue together fields of algebraic theories in order to obtain algebraic theories of more sophisticated arities. My main purpose in this invited talk will be to illustrate the idea with the local state monad, and to explain why the notion of "effect bundle" is critical to the programme of depicting proofs and programs in the functorial language of string diagrams. Short bibliography:

10:30–13:00: STRING workshop

13:00–14:00: Lunch

14:00–15:00: invited talk by Marcelo Fiore, 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 of Baez-Dolan for generating opetopes. The technical work will involve setting up a microcosm principle for near-semirings and subsequently exploiting it in the cartesian closed bicategory of generalised species of structures. Connections to Homotopy Type Theory, (cartesian and symmetric monoidal) equational theories, λ-calculus, and algebraic combinatorics will be mentioned in passing.

15:00–15:30: Maxime Lucas, On the structure of local branchings

Local n-branchings play a central role in higher dimensional rewriting. In this paper we study the structure of these branchings. We define what a presentation of an O-algebra by a rewriting system is, for a general (non-symmetric, set-theoretic) operad O. In this setting, we define what a local n-branching is, and show that they form an O-algebra in the category of augmented symmetric simplicial sets, equipped with the appropriate monoidal structure. In particular when O is the monoid operad, local n-branchings form a monoid in augmented symmetric simplicial sets. Finally we define the notions of aspherical, Peiffer, overlapping and critical branchings in this setting, and recover in good cases some properties expected from the traditional monoid example.

15:30–16:00: Break

16:00–16:30: Thibaut Benjamin, A Type-Theoretical Definition of Weak ω-Functors

The aim of this article is to study the Finster-Mimram type-theoretical definition of weak ω-categories. We first propose a full description of the models of this theory in low dimensional cases. This leads to a combinatorial definition of unbiased categories and unbiased bicategories in terms of globular sets. We then propose an extension to include a type theoretical definition of functors and natural transformations between two such weak omega-categories, and describe the one-dimensional models for the theory of functors, leading naturally to the definition of weak unbiased functors.

16:30–17:00: Amar Hadzihasanovic, A combinatorial-topological shape category for polygraphs

Building on ideas of poset topology, I give a combinatorial description of a class of shapes of higher-categorical cells, with a mild constraint of topological nature (n-boundaries are homeomorphic to n-disks), and good technical properties, such as closure under tensor products. I also report on an associated notion of weak unit cell, obtained from a representability condition, which could bridge the gap with the needs of string diagram rewriting.

17:00–17:30: Simon Forest, A better understanding of structures for pasting diagrams for strict ω-categories

In this work, we give an analysis of the structures introduced by Street, Johnson and Steiner to represent “loop-free” ω-categories using the idea of pasting diagrams. We give elementary conditions that need to be satisfied for these structures to work. One of the condition was not enforced in Street and Johnson, which resulted in examples accepted by their theories that break freeness. Finally, we expose a generalization that encompasses all the structures.

17:30–17:45: Break

17:45–18:15: Domnic Verdon, Coherence for braided and symmetric pseudomonoids

Presentations for unbraided, braided and symmetric pseudomonoids are defined. Biequivalences characterising the semistrict monoidal bicategories generated by these presentations are proven. It is shown that these biequivalences categorify results in the theory of monoids and commutative monoids, and are generalisations of the standard coherence theorems for braided and symmetric monoidal categories.

18:15–18:45: Benjamin Dupont, A convergent presentation for the simply-laced KLR algebra and the PBW property

In higher representation theory, we study actions of algebras on categories rather than vector spaces. Given an algebra presented by generators and relations, we can study its 2-representations by constructing a categorification of the algebra. In a process of categorifying quantum groups linked with symmetrizable Kac-Moody algebras, Khovanov and Lauda introduced, in the same time than Rouquier, the KLR algebras which have the property to act on some endomorphisms spaces of their 2-category. In this work, we use rewriting methods to find explicit bases for the KLR algebras in the simply-laced case. Those bases, called PBW bases by Rouquier, are important to control the size of the spaces of 2-cells in the 2-category. In particular, we construct a convergent presentation of these KLR algebras by a linear (3,2)-polygraph.

18:45–19:15: Andrew Polonsky, Lambda Calculus is a Groupoid!

We present a higher-dimensional analysis of the lambda calculus. Taking equality of lambda terms to be beta conversion modulo permutation of redexes naturally leads to an infinite hierarchy of lambda terms, equalities between terms, equalities between equalities, etc. We show that this hierarchy collapses at level 3. That is, there exist lambda terms with non-equal conversions between them, yet any two 2-cells between the same conversions are equated by a 3-cell. This higher structure thus exhibits the lambda calculus as a homotopy 1-type.

Saturday, September 9th

9:30–10:30: invited talk by Dimitri Ara, Street's orientals and associativity coherences

Orientals were introduced by Street to define a nerve functor from strict ∞-categories to simplicial sets. The n-th oriental is a free strict n-category whose generating cells correspond to the faces of the standard n-simplex. As first observed by Kapranov and Voevodsky, orientals are strongly connected to the geometry of associativity. In particular, Mac Lane's coherence theorem can be stated as a property of orientals. The purpose of our talk will be to explain these connections and to state a conjecture on orientals, introduced in a joint paper with Georges Maltsiniotis, that is in some sense a higher Mac Lane's theorem. This conjecture might be attackable by higher rewriting techniques.

10:30–11:00: Clément Alleaume, Coherent presentations of Karoubi envelopes

We introduce an application of polygraphs to the construction of Karoubi envelopes. We first extend the construction of Karoubi envelope to n-polygraphs. The second problem treated in this paper is the construction from a coherent presentation of an n-category a coherent presentation of its Karoubi envelope. We solve this problem by defining a notion of Karoubi envelope for globular extensions.

11:00–11:30: Break

11:30–12:00: Mauro Jaskelioff, Exequiel Rivas, Tarmo Uustalu and Niccolò Veltri, Coherence for Skew Near-Semiring Categories

We consider skew near-semiring categories, a relaxation of near-semiring categories where the unitors, associators, absorber and distributor are not required to be natural isomorphisms, they are just natural transformations in a particular direction. We prove a coherence theorem for such categories. The theorem states that, in a free skew near-semiring category over a set of objects, any two maps between an object and an object in normal form are equal.

12:00–12:30: Cyrille Chenavier, Upper-bound of reduction operators and computation of syzygies

We are interested in the computation of syzygies of a set of reduction operators, describing linear rewriting rules. The set of reduction operators admits a lattice structure. The lower bound of this structure enables us to compute syzygies for a pair of reduction operators. Using this, as well as an inductive construction, we deduce a method for constructing the syzygies of any finite set of reduction operators.

12:30–13:00: Matteo Acclavio, A constructive proof of coherence for symmetric monoidal categories using rewriting

A symmetric monoidal category is a category equipped with an associative and commutative (binary) product and an object which is the unit for the product. In fact, those properties only hold up to natural isomorphisms which satisfy some coherence conditions. The coherence theorem asserts the commutativity of all linear diagrams involving the left and right unitors, the associator and the braiding. We prove the coherence for symmetric monoidal categories using a constructive homotopical method based on higher dimensional rewriting. For that scope, we detail the convergence proof of Lafont's string diagram rewriting system which presents the isomorphisms of these theories.

13:00–14:00: Lunch

14:00–17:30: STRING workshop


The event will be hosted at the historical Jericho Tavern in the heart of Oxford:

See the FSCD 2017 webpage for more details.

Important Dates

Organization Committee

Program Committee

Past editions