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,

10:30–13:00: STRING workshop

13:00–14:00: Lunch

14:00–15:00: invited talk by Marcelo Fiore,

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

16:30–17:00: 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:00–17: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.

17:30–17:45: Break

17:45–18:15: 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:15–18:45: 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.

Saturday, September 9th

9:00–10:00: invited talk by Dimitri Ara,

10:00–10:30: 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.

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

12:00–12:30: 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:30–13:00: 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.

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