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

## Overview

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

*higher-dimensional rewriting*: extensions of rewriting theory to higher-dimensional settings (operads, opetopes, polygraphs/computads, parity complexes, augmented directed complexes, etc.), generalizations of string/term/graph rewriting systems, etc.*higher categorical structures*: weakening, combination and comparison of categorical structures (monoids, bialgebras, Frobenius algebras, Lie algebras, etc.), coherence theorems, etc.*applications of rewriting to algebraic topology*: construction of resolutions, homotopical and homological invariants, linear rewriting (Gröbner bases, applications to algebras and operads), Koszul duality theory, etc.*applications and interactions with other fields*: calculi for quantum computations, proof nets, algebraic lambda-calculi, topological models for concurrency, homotopy type theory, combinatorial group theory, etc.*implementations*: the workshop will also be interested in implementation issues in higher-dimensional rewriting and will allow demonstrations of prototypes of existing and new tools in higher-dimensional rewriting.

## Invited Speakers

- Dimitri Ara (Aix-Marseille Université)
- Marcelo Fiore (University of Cambridge)
- Paul-André Melliès (CNRS, Université Paris 7)

## Programme

### 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*

## Venue

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

- Paper Submission: June 25, 2017
- Notification of Acceptance: July 10, 2017
- Final version: July 18, 2017
- Conference: September 8-9, 2017

## Organization Committee

- Yves Guiraud (INRIA / Université Paris 7)
`yves.guiraud(@)pps.univ-paris-diderot.fr` - Philippe Malbos (Université Claude Bernard Lyon 1)
`malbos(@)math.univ-lyon1.fr` - Samuel Mimram (École Polytechnique)
`samuel.mimram(@)lix.polytechnique.fr`

## Program Committee

- Yves Guiraud (INRIA / Université Paris 7)
- Philippe Malbos (Université Claude Bernard Lyon 1)
- Paul-André Melliès (Université Paris Diderot)
- Samuel Mimram (École Polytechnique)
- Tim Porter
- Femke van Raamsdonk (VU University, Amsterdam)
- Pawel Sobocinski (University of Southampton)
- Jamie Vicary (University of Oxford)