À l’occasion du départ à la retraite de François Métayer, nous souhaitons rendre hommage à notre collègue et ami, chantre des polygraphes, de l’homotopie et de la réécriture, animateur d’un groupe de travail mythique sur ces sujets. L’événement aura lieu les 8 et 9 juin 2023 et sera précédé par les journées LHC.

In order to celebrate François Métayer, who is going to retire soon, we are organizing special days at IRIF, around the themes of polygraphs, homotopy and rewriting, that he has eminently and magnificently contributed to promote over the years. The event is planned on 8 and 9 June 2023. On the days before, the LHC days will take place and should also be of interest.

Invited speakers

• Albert Burroni, IMJ, UPC
• Léonard Guetta, postdoc au Max Planck Institut, Bonn
• Amar Hadzihasanović , Tallinn University of Technology
• Simon Henry, University of Ottawa
• André Joyal, Université du Québec à Montréal
• Muriel Livernet, IMJ, UPC
• Philippe Malbos, Université Claude Bernard Lyon 1
• Georges Maltsiniotis, IMJ, UPC
• Samuel Mimram, Ecole Polytechnique
• Alain Prouté, membre à la retraite de l’IMJ, UPC

Location

The conference will take place in the amphitheater 4C of halle aux farines:

Preliminary program

Thursday 8

10h André Joyal: The Cyclic Category Revisited

11h Break

11h30 Amar Hadzihasanović: Computational aspects of higher-dimensional rewriting

12h30 Lunch

14h30 Albert Burroni: Essai d’une traduction (partielle) en géométrie polygraphique, des calculs effectués dans les algèbres de Lie

15h30 Short break

15h45 Philippe Malbos: Resolutions and abstract abstract coherence

16h45 Break

17h15 Alain Prouté: Une approche nouvelle de la notion de preuve

Friday 9

9h30 Simon Henry: Strictification for dependently typed algebraic theories

10h30 Break

11h Muriel Livernet: A walk on the edges of simplices and cubes or how to build an equivalence between models of ∞-categories?

12h Lunch

14h Georges Maltsiniotis: Homologie polygraphique d’un système local

15h00 Short break

15h15 Léonard Guetta: Homologie polygraphique des 1-catégories à coefficients dans un système local

16h15 Break

16h45 Samuel Mimram: Polygraphs in homotopy type theory

Abstracts

Albert Burroni: Essai d’une traduction (partielle) en géométrie polygraphique, des calculs effectués dans les algèbres de Lie / slides

(avec la collaboration de Pierre-Louis Curien)

Depuis Descartes au moins, on sait que l’algèbre et la géométrie sont deux faces « duales » d’un même univers mathématique. Par exemple, le concept de crochet de Lie est lié à l’idée de courbure d’une variété différentielle.

Malgré mon désir de les connaître je n’ai jamais eu l’occasion de travailler ni sur les algèbres de Lie, ni même (en dehors de ma période étudiante) sur la géométrie différentielle. Pourtant désirant trouver des applications à la notion de polygraphe, un jour par hasard, j’ai remarqué (remarque très banale) que la forme de l’identité de Jacobi dans les algèbres de Lie, évoque celle d’un cube polygraphique. A partir de là, j’ai laissé libre cours à des investigations qui relèvent de la réécriture en dimensions supérieure et qui, je l’espère, ne propose ici qu’un début. Il faut toutefois beaucoup de concessions de la part des deux camps, l’algèbre n-Lie-esque (comme dirait Pierre-Louis) et la n-polygraphie, pour que l’aventure aie des lendemains.

Léonard Guetta: Homologie polygraphique des 1-catégories à coefficients dans un système local / slides / article

Cet exposé fait suite à celui de G. Maltsiniotis et reprend la notion d’homologie polygraphique à coefficients dans un système local. On se restreindra au cas de l’homologie des (1-)catégories et on montrera le résultat de comparaison suivant : pour toute petite catégorie C et tout système local M sur cette dernière, l’homologie polygraphique de C à coefficients dans M est canoniquement isomorphe à l’homologie du nerf de C à coefficients dans M, généralisant ainsi le cas classique des coefficients constants à valeur dans ℤ.

Amar Hadzihasanović: Computational aspects of higher-dimensional rewriting / slides

I will report on my joint work with Diana Kessler on the algorithms and complexity theory of higher-dimensional rewriting. In particular, I will focus on the subdiagram matching problem, that is, the problem of matching an n-dimensional diagram to a “rewritable portion” of another n-dimensional diagram. I will present the relevant data structures, based on the combinatorial theory of diagrammatic sets, outline an algorithm valid in all dimensions, and show how it can be simplified up to dimension 3. If possible, I will accompany parts of the presentation with a demonstration of rewalt, an implementation of our data structures in Python.

Simon Henry: Strictification for dependently typed algebraic theories

For a dependently typed algebraic theory T (a generalized algebraic theory in the sense of Cartmell), I will show how to build a model category of simplicial T-models and show that it is equivalent to a good notion of “weak topological models of T” (that is model up to homotopy). This is a generalization of a theorem of Badzioch for Lawvere theories.

In the special case where the category of (set-valued) models of T already carries a nice model structure, for example, when T is the theory of strict ∞-categories, I will also connect this model structure with these weak topological models.

André Joyal: The Cyclic Category Revisited / slides

Connes cyclic category is a full subcategory of the category of n-categories. I will describe its application to the construction of universal traces and to the construction of free compact-closed ∞-categories. This joint work with Amit Sharma.

Muriel Livernet: A walk on the edges of simplices and cubes or how to build an equivalence between models of ∞-categories?

In this talk I will explain a combinatorial method for comparing different models of ∞-categories, due to Dugger and Spivak for the cases of simplicial sets. We will apply it to the case of cubical sets and see that the combinatorics involves the weak Bruhat order on the symmetric group. This is a joint work with Pierre-Louis Curien and Gabriel Saadia.

Philippe Malbos: Resolutions and abstract abstract coherence / slides

The notion of resolution by polygraphs of higher categories introduced by François Métayer has led to the formulation of several problems at the interface of higher dimensional rewriting and homotopical algebra. In particular, the computation of polygraphic resolutions by confluence and the definition of algebraic variants lead to difficult and still open problems in many algebraic contexts.

In this talk, I will discuss a new line of study of polygraphic resolutions with the question of their algebraic formalisation, in view of their formalisation in proof assistants. I will show how to formalize some polygraphic concepts in higher Kleene algebras, as well as polygraphic resolutions in low dimension.

Georges Maltsiniotis: Homologie polygraphique d’un système local / article

Dans cet exposé, après avoir rappelé la définition de l’homologie d’un espace topologique ou d’un ensemble simplicial à coefficients dans un système local, on introduira une notion d’homologie polygraphique d’une ∞-catégorie stricte à coefficients dans un tel système, généralisant ainsi l’homologie polygraphique à coefficients dans ℤ, introduite par François Métayer. On montrera que l’adjoint à gauche du nerf de Street respecte cette homologie.

Samuel Mimram: Polygraphs in homotopy type theory / slides

In homotopy type theory, higher inductive types provide us with a notion of polygraph adapted to expressing presentations of weak ∞-groupoids. I will review two methods for constructing such polygraphs, in the case of presentations of groups. The first one, due to Kraus and von Raumer, is a direct adaptation of the traditional rewriting techniques and allows computing the generators for coherence in (very) low dimensions. The second one, due to Rijke, uses the join construction in order to generate coherences all the way up, thus computing a “polygraphic resolution” of the group. I will illustrate the use of those constructions on examples.

Alain Prouté: Une approche nouvelle de la notion de preuve / article

Je propose un façon nouvelle d’aborder la notion de preuve formelle qui ne suppose aucune syntaxe a priori pour les preuves et qui n’utilise aucun des travaux des logiciens de Gentzen à Howard, mais uniquement des faits élémentaires et indiscutables pour les mathématiciens non logiciens. Le résultat ressemble, on s’en doute, à ce qui est proposé par l’isomorphisme de Curry-Howard, mais avec certaines différences. Par ailleurs, cette approche me semble mieux justifiée que l’approche traditionnelle pour des raisons de méthodologie que j’expliquerai.

Participants

• Quentin Aristote (IRIF)
• Nicolas Behr (CNRS, IRIF, Université Paris Cité)
• Thibaut Benjamin (University of Cambridge)
• Arij Benkhadra (Université de Paris Nanterre)
• Clemens Berger (Université Côte d’Azur)
• Victor Brittes (Université Côte d’Azur)
• Hugo Cadière (Université Jean Moulin lyon 3)
• Cameron Calk (Laboratoire d’Informatique et Systèmes (Univ. Aix-Marseille))
• El Mehdi Cherradi (IRIF)
• Younggi Choi (Seoul National University, Department of Mathematics Education)
• Bryce Clarke (Inria Saclay)
• Sophie d’Espalungue (Paris Cité)
• Marc de Visme (Loria, Nancy)
• Bérénice Delcroix-Oger (IMAG, Université de Montpellier)
• Raffaele Di Donna (IRIF, Université Paris Cité, Università Roma Tre)
• Sylvain Douteau (IRIF)
• Aloÿs Dufour (Université Paris-Nord)
• Thomas Ehrhard (IRIF)
• Raül Espejo Boix (Université de Rennes 1 et IRISA)
• Uli Fahrenberg (LRE, EPITA)
• Eric Finster (University of Birmingham)
• Zeinab Galal (LIP6, Sorbonne Université)
• Guillaume Geoffroy (Université Paris Cité - IRIF)
• Léonard Guetta (Max-Planck-Institut für Mathematik)
• Pierre Giraud (équipe Gallinette, INRIA (centre de Rennes –Loire atlantique) (hébergé à Nantes Université))
• Eric Goubault (LIX, Ecole polytechnique)
• Adrien Guatto (IRIF)
• Amar Hadzihasanovic (Tallinn University of Technology)
• Hélène Han (IRIF (en stage de M1))
• Elies Harington (Ecole Polytechnique)
• Grant Harvey (Queen’s University Belfast)
• Hugo Herbelin (IRIF - INRIA)
• Eric Hoffbeck
• Léo Hubert (Aix Marseille Université)
• Moana Jubert (IRIF, Inria, CNRS, Université Paris-Cité)
• Stefano Kasangian (Università di Milano)
• Roman Kniazev (LIX)
• Praphulla Koushik (IISER Pune)
• Adrienne Lancelot (INRIA & Lix)
• Samuel Lavenir (EPFL)
• Louis Lemonnier (LMF, Université Paris-Saclay)
• Quan Long (ENS Paris Saclay)
• Felix Loubaton (Université Côte d’Azur)
• Luidnel Maignan (LMF/ENS Paris-Saclay & LACL/Univ. Paris-Est Créteil)
• Georges Maltsiniotis (IMJ-PRG)
• Aníbal Medina (Paris 13)
• Thomas Jan Mikhail (Autonomous University of Barcelona)
• Mariana Milicich (UPC)
• Samuel Mimram (École polytechnique)
• Marianela Morales (INRIA Saclay & École Polytechnique)
• Vincent Moreau (IRIF, Université Paris Cité, Inria Paris)
• François Métayer (IRIF)
• Axel Osmond (Institut Grothendieck)
• Stiéphen Pradal (University of Nottingham)
• Francesca Pratali (Université Sorbonne Paris Nord)
• Manuel Rivera (Purdue University)
• Paul Ruet
• Gabriel Saadia (Stockholm University)
• Elena Sendroiu (Independent researcher)
• Lutz Strassburger (Inria Saclay)
• Alexis Terrassin (Université Paris Cité)
• Gérard Varacca (Paris Saclay)
• Vladimir Zamdzhiev (Inria)
• Noam Zeilberger (LIX)

Organizing team

• Dimitri Ara (Aix-Marseille Université)
• Pierre-Louis Curien (CNRS & Université Paris Cité)
• Yves Guiraud (Inria & Université Paris Cité)
• Yves Lafont (Aix-Marseille Université)