Working group

Inria project-team $\pi r^2$ (Inria)
Thematic team Algebra and computation

Day, hour and place

Friday at 2pm, room 1007

The calendar of events (iCal format).
In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.


Higher categories, polygraphs and homotopy
Friday April 19, 2024, 2PM, Salle 3058
Jovana Obradovic A Calculus for S^3-diagrams of Manifolds with Boundary

n this talk, we shall introduce a calculus for a presentation of compact, orientable, connected 3-manifolds with boundary in terms of diagrams embedded in S^3 in a form akin to the standard surgery presentation of closed, orientable, connected 3-manifolds. The motivation to introduce such a presentation of manifolds is to give a completely combinatorial description of the category 3Cob, whose arrows are 3-dimensional cobordisms, which is an ongoing project. We hope this could support further investigations of faithfulness of 3-dimensional Topological Quantum Field Theories.

This is a joint work with Bojana Femić, Vladimir Grujić and Zoran Petrić.

Higher categories, polygraphs and homotopy
Friday May 31, 2024, 2PM, Salle 3058
Sacha Ikonicoff Catégories différentielles et tangentes pour les algèbres sur une opérade

La notion de catégorie différentielle cartésienne permet de formaliser dans un contexte catégorique la notion de dérivée directionnelle. Similairement, la notion de catégorie tangente fournit un analogue à la notion de fibré tangent de la géométrie différentielle dans le contexte de la théorie des catégories.
  Dans cet exposé, nous décrirons une nouvelle notion de monade différentielle cartésienne. Cette structure consiste en une monade équipée d'une transformation naturelle appelée "combinateur différentiel". Pour une telle monade, nous montrerons que la catégorie (opposée) de Kleisli associée est munie d'une structure différentielle cartésienne, et que la catégorie d'algèbres associée est munie d'une structure tangente.
  Finalement, nous considérerons l'exemple des algèbres sur une opérade. Nous montrerons que la monade associée à toute opérade (algébrique, symétrique) admet un combinateur différentiel. Nous étudierons la catégorie différentielle cartésienne et la catégorie tangente associée. Nous montrerons que cette catégorie tangente admet une structure tangente adjointe qui permet de retrouver certaines notions provenant de la géométrie algébrique et non-commutative.

Year 2024

Higher categories, polygraphs and homotopy
Friday April 12, 2024, 2PM, Salle 3058
Fabio Gadducci (University of Pisa) From monoidal to cartesian categories: a computational view

It is well-known that the arrows of the free cartesian category C(S) over a signature S are (tuples of) terms built over S, and that cartesian functors from C(S) into Set corresponds algebras over S. A term-like structure is also available for the arrows of some free categories over S laying between the free monoidal and the free cartesian categories, and suitable functors into Rel and Par can also be interpreted as multi- and partial algebras, respectively. Finally, all these categories can be obtained as the Kleisli category of suitable monads, hence offering a tool for the “computations and monads” paradigm.

Higher categories, polygraphs and homotopy
Friday April 5, 2024, 2PM, Salle 3058
Yonatan Harpaz Lax limits of model categories

In higher category theory, model categories constitute a powerful manner to encode infinity categories. Unfortunately, it is not always possible to encode an infinity category using a model category, and when this is possible the choice of model category is far from being unique or canonical. Favoring such presentations whenever possible, it is hence natural to investigate which operations on the level of infinity categories can be performed on the model categorical level. In this talk I will describe one such result for the operation of lax limits, showing that, under suitable conditions, if a diagram of inifinity categories is modeled by a diagram of (simplicial combinatorial) model categories, then the lax limit can be performed on the level of model categories. We also obtain results concerning homotopy limits and various intermediate limits. This generalizes previous results of Lurie and of Bergner. Related results were also obtained independently by Balzin.

Higher categories, polygraphs and homotopy
Friday March 22, 2024, 2PM, Salle 3058
Sophie D'Espalungue (Université de Lille) Une théorie hiérarchique des types, ou théorie formelle des catégories (supérieures)

Je propose la notion d'un système de types hiérarchiques, de sorte que la définition soit elle même exprimée de manière interne au système qu'elle définit. L'idée est qu'un tel système fournit un cadre au sein duquel on peut raisonner, tout en possédant sa propre logique. On pourra établir des constructions formelles en se plaçant dans un système quelconque et en déduire des résultats généraux. On définira notamment la notion de oméga type dans un système. On verra que le cas non trivial minimal émane naturellement de la logique booléenne habituelle et fournit la hiérarchie des n-catégories. On remarquera la nature intrinsèquement homotopique du cadre ainsi obtenu, si bien que les oméga types de ce système peuvent naturellement s'interpréter comme des espaces. J'aimerai aussi revenir sur quelques axiomes de la théorie homotopique des types et de la théorie des ensembles.

Higher categories, polygraphs and homotopy
Friday March 8, 2024, 2PM, Salle 3058
Emile Oléon (Ecole polytechnique) Delooping cyclic groups with lens spaces in homotopy type theory

In the setting of homotopy type theory, each type can be interpreted as a space. Moreover, given an element of a type, i.e. a point in the corresponding space, one can define another type which encodes the space of loops based at this point. In particular, when the type we started with is a groupoid, this loop space is always a group. Conversely, to every group we can associate a type (more precisely, a pointed connected groupoid) whose loop space is this group: this operation is called delooping. The generic procedures for constructing such deloopings of groups (based on torsors, or on descriptions of Eilenberg-MacLane spaces as higher inductive types) are unfortunately equipped with elimination principles which do not directly allow eliminating to arbitrary types, and are thus difficult to work with in practice. Here, we construct deloopings of the cyclic groups Z_m which are cellular, and thus do not suffer from this shortcoming. In order to do so, we provide type-theoretic implementations of lens spaces, which constitute an important family of spaces in algebraic topology. In some sense, this work generalizes the construction of the real projective space by Buchholz and Rijke in their LICS'17 paper, which handles the case m=2, although the general setting requires more involved tools. Finally, we use this construction to also provide cellular descriptions of dihedral groups, and explain how we can hope to use those to compute the cohomology and higher actions of such groups.

Higher categories, polygraphs and homotopy
Friday February 9, 2024, 2PM, Salle 3058
Louise Leclerc (ENS) Diverses formulations des opétopes (positifs), et leur équivalences

L'idée est de présenter quelques formalisations des opétopes (entre 3 et 4…) avec lesquelles j'ai pu travailler durant mon stage. Et notamment d'introduire des définitions originales de Pierre-Louis Curien et moi. Je ne pense pas parcourir la preuve de l'équivalence, éventuellement donner des idées vagues de ce qu'il faut faire pour les relier.

Si le temps le permet, je pourrait aussi introduire une définition pour les opétopes (non nécessairement positifs cette fois) à laquelle j'ai réfléchi dernièrement, et dont j'ai démontré l'équivalence avec les “Zoom complexes” du papier “Polynomial functors and opetopes” par Kock, Joyal, Batanin et Mascari.

Year 2023

Higher categories, polygraphs and homotopy
Friday September 15, 2023, 2PM, Salle 165 - Olympe de Gouges
Lukas Waas (Heidelberg University) From stratified spaces to layered infinity-categories

To a topological space one may associate an infinity-groupoid of paths, with objects given by points, 1-morphisms given by paths, 2-morphisms given by homotopies, and so on. It is a result due to Kan and Quillen - sometimes called the homotopy hypothesis - that this construction induces an equivalence between the homotopy theory of CW-complexes and infinity-groupoids. The stratified world admits a similar construction, the infinity-category of exit paths, which associates to a sufficiently regular stratified space (such as a pseudo manifold) an infinity-category given by paths which ascend in the stratification. It was conjectured by Ayala, Francis and Rosenblyum that this construction induces an equivalence between a homotopy theory of appropriate topological stratified spaces (obtained by inverting stratified homotopy equivalences) and so called layered infinity-categories (such infinity categories in which every endomorphism is an isomorphism). In this talk, we are going to provide an affirmative answer to this conjecture. Namely, we identify a category of stratified spaces, which contains classical examples such as piecewise-linear pseudo-manifolds, such that its localization at stratified homotopy equivalences is equivalent to the homotopy theory of small layered infinity-categories, via the exit-path construction.

Higher categories, polygraphs and homotopy
Friday June 30, 2023, 2PM, salle 163 (Olympe de Gouges)
Peter Faul (LIX) Cyclic Polycategories: Completing the Contour/Splice Adjunction

In this talk we consider generalisations of the Word-Splice/Contour Adjunction between Categories and Multicategories, introduced by Paul-André Melliès and Noam Zeilberger. We observe that the counit is 'almost' invertible, failing only to be full for a fairly trivial reason. This trivial reason can be circumvented by generalising the construction to polycategories. We also observe that the word-splice functor always supplies cyclic multicategories. This motivates cyclic polycategories as the most appropriate setting in which to consider this adjunction.

However there are a number of ways in which we could consider a polycategory to be cyclic. In this talk we discuss two such ways, where in the one we impose a duality condition and in the other we do not. We end by discussing some links between these cyclic polycategories and cyclic linear logic

Higher categories, polygraphs and homotopy
Friday June 2, 2023, 2PM, salle 147 (Olympe de Gouges)
Noam Zeilberger (LIX) Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem

The classical statement of the Chomsky-Schützenberger representation theorem says that any context-free language may be represented as the homomorphic image of the intersection of a Dyck language of balanced parentheses with a regular language. In the talk I will discuss a fibrational perspective on context-free grammars and finite-state automata that grew out of a long-running project with Paul-André Melliès on type refinement systems, but with a surprising twist that only emerged when we considered the C-S theorem. It turns out that underlying that theorem is a basic adjunction between categories and colored operads (= multicategories), where the right adjoint $W : Cat \to Oper$ builds a “spliced arrow operad” out of any category, and the left adjoint $C : Oper \to Cat$ sends any operad to a “contour category” whose arrows have a geometric interpretation as oriented contours of operations.

Based on joint work with Paul-André Melliès that appeared at MFPS 2022 (, as well as a long version of that article in preparation.

Higher categories, polygraphs and homotopy
Friday April 28, 2023, 2PM, Salle 146 Olympe de Gouges
Morgan Rogers Endomorphismes de modèles

Un résultat classique mais peu connu de la théorie des modèles donne une correspondance entre des structures relationnelles sur un ensemble et les sous-groupes fermés de son groupe topologique d'automorphismes. Avec la théorie des (1)-topos classifiant, on peut étendre ce théorème, remplaçant “ensemble” par “modèle d'une théorie géométrique quelconque”, et si on le veut, “groupe” par “monoïde”. Je vais expliquer ce résultat et, le temps permettant, considérer comment l'étendre aux (infini,1)-topos.

Higher categories, polygraphs and homotopy
Friday April 21, 2023, 2PM, Salle 146 Olympe de Gouges
Uwe Wolter (University of Bergen) An Outline of the Theory of Generalized Sketches

Based on a new concept of first-order generalized sketches we coined lately “Logics of Statements in Context” to provide a unified view on formalisms like Algebraic Specifications, Prolog, First-Order Logic, Ehresmann Sketches, Description Logics, Generalized Sketches à la Makkai/Diskin, Diagram Predicate Framework, Graph Conditions, and others. In the talk we present Generalized Sketches à la Makkai/Diskin as a quite natural generalization of traditional Ehresmann sketches. Generalized Sketches à la Makkai/Diskin can be defined in arbitrary categories. They built upon “atomic statements in context” and utilize sketch implications for axiomatization purposes. Going beyond atomic statements, we outline the definition of arbitrary first-order statements in arbitrary categories enabling us to enhance the expressiveness of Generalized Sketches. In analogy to first-order statements, we can also define arbitrary first-order sketch conditions generalizing thereby different kinds of “nested graph constraints and conditions”.

We intend to discuss, on the way, two essential constructions Makkai’s work on Generalized Sketches relies on: “Syntactic representation of models” and “internalization of atomic statements”.

Zoom meeting registration link :

Séance conjointe avec le séminaire Graph Transformation Theory and Applications

Attention au changement de salle consécutif aux travaux !

Higher categories, polygraphs and homotopy
Friday March 17, 2023, 2PM, Salle 1007
Uli Fahrenberg (Epita) 2-Categories with Lax Tensors, With a Motivation from Concurrency Theory

Concurrent Kleene algebra, introduced by Tony Hoare in 2011, extends Kleene algebra with a parallel composition operator. The result is a double monoid with a lax interchange law between concatenation (i.e. serial composition) and parallel composition. Its free models are series-parallel pomsets, that is, partial strings which a freely generated from the alphabet by binary serial and parallel composition.

We have recently had occasion to consider a generalisation of serial composition where events in pomsets may continue across compositions. The resulting algebraic structure is a 2-category with a form of lax tensor; for the time being it is not clear what are its free models, nor whether they even exist. Further, ultimately we is interested in languages of pomsets, and lifting 2-categories (or just categories) across the powerset functor has turned out to be interesting just in and of itself.

Joint work with Christian Johansen, Georg Struth and Krzysztof Ziemiański. References: - Posets With Interfaces as a Model for Concurrency. Information and Computation 285(B):104914 (2022). - Catoids and Modal Convolution Algebras. Algebra Universalis 84(10) (2023).

Higher categories, polygraphs and homotopy
Friday February 24, 2023, 2PM, Salle 1007
Bartosz Milewski Compound optics

The action of a bicategory generalizes monoidal action and leads to a bicategory of compound optics. These optics are expressed using coends; they also have Tambara representations.

Higher categories, polygraphs and homotopy
Friday February 17, 2023, 2PM, Salle 1007
Bryce Clarke (INRIA Saclay) The right-connected completion of a double category

Double categories are a two-dimensional structure consisting of objects, two classes of morphisms (horizontal and vertical), and cells between them. A double category may be defined as an internal category in CAT, and it is called right-connected if its identity-assigning map is right adjoint to its codomain-assigning map. The intuition is that every vertical morphism in a right-connected double category has an underlying horizontal morphism. Right-connected double categories play an important role in the characterisation of algebraic weak factorisation systems, and this motivates the question: is it possible to complete a double category under the property of right-connectedness?

In this talk, I will provide an explicit characterisation of the right-connected completion of a double category, and study its properties. I will examine several examples of right-connected double categories arising from this completion, and show how particular instances lead to examples of algebraic weak factorisation systems. The main theorem of the talk will provide conditions for a double category arising from the right-connected completion to be comonadic (in a suitable sense) over the original double category.

Higher categories, polygraphs and homotopy
Friday February 10, 2023, 2PM, Salle 1007
El Mehdi Cherradi (IRIF) La structure de modèle “smothering” sur Cat et les semidérivateurs comme (oo,1)-catégories

La notion de foncteur “smothering” (étouffant en français …), introduite par Riehl et Verity, apparaît fréquemment en homotopie, par exemple le foncteur de comparaison entre la catégorie homotopique de $Ho(C^\rightarrow)$ et la catégorie de flèche $Ho(C)^\rightarrow$ pour toute quasicatégorie $C$. Une légère variation de cette notion se trouve définir la classe d'équivalence faible d'une localisation de Bousfield à droite de la structure de modèle naturelle sur Cat. Le but de l'exposé est d'illustrer l'importance de cette structure en définissant une structure de modèle induite sur la catégorie des semidérivateurs montrant que ces derniers modélisent les $(\infty,1)$-catégories.

Higher categories, polygraphs and homotopy
Friday February 3, 2023, 2PM, Salle 1007
Pierre-Louis Curien & Guillaume Laplante-Anfossi (IRIF & Melbourne University) Une preuve simple et connexe du théorème de cohérence de MacLane

Bien que le théorème de cohérence de MacLane pour les catégories monoïdales ait été prouvé initialement par une méthode proche de la réécriture, il présente un caractère topologique. C’est ce qui a poussé Kapranov à suggérer en 1993 une « preuve instantanée » de ce théorème basée sur l’existence d'une famille de polytopes qu’il nomme permutoassociaèdres. Dans la première partie, on formalisera cette idée, montrant que la cohérence de MacLane est une conséquence directe de la simple connexité des permutoassociaèdres. Cela suggère un lien combinatoire plus général entre cohérence n-catégorique et n-connexité de certains espaces, avatar « strict » de travaux infini-catégoriques récents de Shaul Barkan.

Dans la deuxième partie, on s'intéressera à l'instanciation du théorème général à la classe des “hypergraph polytopes” (aussi connus sous le nom de nestoèdres), dont les faces (et en particulier les sommets et les arêtes) sont décrits par des objets combinatoires appelés “constructs”. Les arêtes sont naturellement orientées à l'aide d'un ordre appelé ordre de Tamari généralisé, et lorsqu'on instancie encore davantage, à la classe des opéraèdres, on obtient un système de réécriture de termes convergent (sous-jacent au problème de cohérence des opérades catégorifiées de Dosen et Petric), ce qui permet dans ce cas d'obtenir la cohérence par des méthodes de réécriture (complétion de Squier). Les diagrammes obtenus sont légèrement différents de ceux de Dosen et Petric.

Higher categories, polygraphs and homotopy
Friday January 27, 2023, 2PM, Salle 1007
François Métayer (IRIF) Les orientaux comme algèbres libres d'une monade

Je présenterai un travail récent en collaboration avec Dimitri Ara et Yves Lafont sur une approche des orientaux de Street proposée par Albert Burroni. Nous décrirons une monade T sur la catégorie des omega-catégories strictes construisant la suite des orientaux par itération à partir de la catégorie initiale.

Year 2022

Higher categories, polygraphs and homotopy
Friday December 9, 2022, 2PM, Salle 1007
Manuel Araujo (Cambridge University) String diagrams for n-sesquicategories

I will talk about work in progress on a theory of semistrict n-categories, where composition is strictly associative and unital, but the interchange laws hold up to coherent equivalence. The idea is to define a semistrict n-category as something which admits composites for labelled string diagrams. The first step is to develop a theory of n-sesquicategories. These encode only the compositional structure of string diagrams, without the interchange laws. I will explain how to define these as algebras over a globular operad whose operations are simple string diagrams, and how to prove that the associated category of computads is a presheaf category. The second step, which is still work in progress, is to add operations implementing the interchange laws up to coherent equivalence, obtaining the desired notion of semistrict n-category. In dimension 3, this recovers the notion of Gray 3-category. ;

Higher categories, polygraphs and homotopy
Friday December 2, 2022, 2PM, Attention changement de salle ! l'exposé a lieu en 4052
Nicolas Behr (IRIF) Double-categorical Compositional Rewriting Theory

Reporting on recent results of joint work with R. Harmer, P.-A. Melliès and N. Zeilberger, I will present a novel formalization of compositional rewriting theory via double categories. For a given rewriting theory, individual rewriting steps are formalized as 2-cells of a double category. One of the crucial aspects of compositionally consists then in providing a set of axioms that the double category of the rewriting system must satisfy in order to ensure the existence of concurrency and associativity theorems, which are quintessential for developing important applications of rewriting systems such as in combinatorics and Markov chain theory. Another concept central to this end, i.e., “counting modulo universal properties”, may be implemented via a certain presheaf and coend calculus. Finally, I will sketch how the counting calculus then leads to a categorification of the concept of rule algebras (which capture the combinatorics of interactions of rewriting steps).

Higher categories, polygraphs and homotopy
Friday November 4, 2022, 2PM, Salle 1007
Léonard Guetta (Max Planck Institute, Bonn) Les préfaisceaux en groupoïdes comme modèles des types d'homotopie

Le but de cet exposé est de présenter le résultat suivant : pour toute catégorie test A, la catégorie des groupoïdes internes à la catégorie des préfaisceaux sur A modélise les types d'homotopie, et ce de manière “canonique”. Il s'agit donc d'une généralisation du résultat de Crans-Joyal-Tierney qui traitait le cas simplicial, lui-même généralisation du résultat célèbre de Kan qui affirme que la catégorie des groupes simpliciaux modélise les types d'homotopie pointés connexes, version non-abélienne de l'équivalence de Dold-Kan.

Comme nous le verrons dans l'exposé, l'intérêt principal du résultat précédent est l'axiomatisation précise de ce qui est entendu par “canonique”, qui constitue une généralisation de la théorie des catégories tests de Grothendieck.

Higher categories, polygraphs and homotopy
Friday October 14, 2022, 2PM, Salle 1007
El Mehdi Cherradi (IRIF) Une sémantique infini-catégorique de la théorie des types basée sur le plongement de Yoneda

Le but de l'exposé est d'expliquer comment construire un modèle de la théorie des types de Martin-Löf à partir d'une infini-catégorie. Le plongement de Yoneda infini-catégorique permet de remplacer une quasicatégorie C par une catégorie simplicialement enrichie équivalente C'. Cette version rigidifiée est par ailleurs une sous-catégorie pleine d'une catégorie de modèle avec d'excellentes propriétés, si bien qu'il est possible, en rajoutant des objets à C', de construire une tribu (au sens de Joyal) C'' toujours équivalente à C et permettant d'interpréter la théorie des types. En particulier, en partant d'un topos élémentaire supérieur, on obtient un modèle de la théorie homotopique des types (HoTT).

Higher categories, polygraphs and homotopy
Friday October 7, 2022, 2PM, Salle 1007
Pierre-Louis Curien (IRIF) Une preuve élémentaire de ce que les ensembles opétopiques sont les polygraphes ``many-to-one’’

Le but de l’exposé est de montrer une définition des opétopes qui prend à la lettre l'approche polynomiale itérée de Kock-Joyal-Batanin-Mascari: un n-opétope est un arbre dont les nœuds et les arêtes sont décorés par des (n-1)-opétopes et des (n-2)-opétopes, récursivement, avec des conditions de recollement. Dans cette approche, distillée de mon travail syntactical-déductif avec Cédric Ho Thanh et Samuel Mimram, tout comme dans ce travail précédent (que je n’aurai pas besoin de rappeler), le codomaine d’un opétope n’est pas une donnée primitive, mais se calcule. Je montrerai comment se fait ce calcul (j'exhiberai en particulier une petite «machine abstraite» qui fait le job), et le lien avec les «flags» dans les présentations combinatoires des opétopes que l’on a pu voir dans l’exposé de Marek Zawadowski (je rappellerai ce dont j’ai besoin). Le clou du spectacle sera le «passage au Bureau International des Poids et Mesures » (je cite ici encore Marek!), pour obtenir l’estampille validant cette définition: les préfaisceaux sur la catégorie des opétopes ainsi définie, ou ensembles opétopiques, sont à iso près les polygraphes «many-to-one» (mto). La structure de la preuve que je présente est exactement celle de Cédric dans sa thèse, mais le lemme clé de cette preuve, qui affirme qu’il y a bijection entre n-cellules d’un polygraphe mto et les arbres dont les nœuds sont décorés par des n-cellules génératrices et les arêtes par des (n-1)-cellules génératrices, reçoit maintenant une preuve élémentaire et explicite.

transparents de l'exposé :

Higher categories, polygraphs and homotopy
Friday September 23, 2022, 2PM, Salle 1007
Marek Zawadowski (Université de Varsovie) (Positive) Opetopes and opetopic sets

In my talk I will review some developments concerning opetopic sets.

Opetopic sets were introduced by J. Baez and J. Dolan in 1998 as a convenient tool to define the notion of a (weak) higher dimensional category. Now we know that the category of opetopic sets is equivalent to the category of many-to-one polygraphs. Opetopes form a small category so that the category of opetopic sets is equivalent to the category of presheaves on the category of opetopes. Since then more than a dozen very different in spirit definitions of opetopes and opetopic sets have been given.

In my talk I will review some of those definitions that can be divided into four groups through the tools deployed: categorical, operadic/monadic, combinatorial, and logical.

In the second part of my talk I will present in detail my combinatorial definitions of (positive) opetopes and some results concerning the category of (positive) opetopic sets such as the monadicity of strict omega-categories over them and that with some degeneracies added positive opetopes form a test category. I will also explain the duality between positive opetopes with epi-contractions maps and the category of Kock-Joyal-Batani-Mascari positive zoom complexes with some fairly natural morphisms between them.

If time permits, I will say something about possible definitions of opetopic categories, i.e., higher dimensional categories based on opetopic sets.

Higher categories, polygraphs and homotopy
Friday June 17, 2022, 2PM, Salle 1007
Cyrille Chenavier (Université de Limoges) Presenting isomorphic finitely presented modules by equivalent matrices: a constructive approach

A multidimensional linear system can be studied by means of its associated module, presented by the unknown functions of this system subject to the equations. Testing whether two linear systems/modules are isomorphic (the so-called equivalence problem) is an important issue. In this presentation, I will first recall from a previous work of Thomas Cluzeau and Alban Quadrat an explicit characterisation for a module morphism to be an isomorphism. Then, I will recall how they obtained a constructive version of a result due to Fitting, which shows how to enlarge matrices presenting isomorphic modules by blocks of zeros and identities to get equivalent matrices. Finally, I will present an inductive procedure for reducing the size of these two equivalent matrices. It turns out that this procedure enables us to recover a result due to Warfield.

Higher categories, polygraphs and homotopy
Friday June 10, 2022, 2PM, Salle 1007
Sylvian Douteau (Stockholm University) Théories de l'homotopie stratifiée : constructions et comparaison

La théorie des espaces stratifiés a des origines très géométriques : le théorème de Whitney garantit que toute variété singulière peut être décomposée en strates qui sont chacune des variétés lisses. Depuis, l'étude des espaces stratifiés, et de leurs invariants, a poussé a considérer des notions plus générales d'espaces stratifiés et a étudier les théories de l'homotopie associées. Pour construire une théorie de l'homotopie stratifiée - en raisonnant par analogie avec la théorie de l'homotopie des espaces - on peut envisager deux approches distinctes. On peut travailler simplicialement pour définir une structure à la Kan, ou bien travailler topologiquement pour définir une structure à la Serre. Dans le cas des espaces, on sait que les théories de l'homotopie obtenues ainsi sont équivalentes. Dans cet exposé, je présenterai des versions stratifiées de ces constructions, et expliquerai pourquoi l'équivalence entre les points de vue simpliciaux et topologiques subsiste pour les espaces stratifiés, mais sous une forme plus subtile.

Higher categories, polygraphs and homotopy
Friday April 15, 2022, 2PM, Salle 1007
Axel Osmond 2-catégories bi-accessibles et biprésentables

Nous introduisons des analogues 2-dimensionels des catégories accessibles et localement présentables.

Récemment, la théorie des pseudofoncteurs plats de Dubuc, Descotte et Szyld a établi l'équivalence entre les pseudofuncteurs dont la bi-exension de Kan à gauche préserve les bilimites finiment pondérées, et ceux dont la (2-catégorie opposée de la) 2-catégories des éléments satisfait une condition de “sigma-filtration” relativement aux morphisms cocartésiens. Ce résultat repose sur le formalisme des sigma-colimites, une construction 2-dimensionnelle à mi-chemin entre les bicolimites et les oplax-bicolimites, et la possibilité de décomposer tout pseudofoncteur à valeur dans Cat comme une sigma-bicolimite de représentables - la partie lax prenant en charge les données 2-dimensionnelles.

Dans cet exposé, nous discutons d'abord de différentes notions de filtration 2-dimensionelles ; nous montrons que toute 2-catégorie sigma-filtrée au sens de Dubuc contient une sous-2-catégorie bifiltrée au sens de Kennisson satisfaisant une condition appropriée de sigma-cofinalité, et que le théorème de décomposition des pseudofoncteurs plats de Dubuc peut se reformuler en un théorème de décomposition en bicolimite bifiltrée de représentables.

Il est donc suffisant de définir les 2-catégories finiment bi-accessibles au moyen des bicolimites bifiltrées et de la notion correspondante d'objet bicompact: nous pouvons montrer alors que ce sont exactement les catégories de pseudofoncteurs plats ; en particulier, nous pouvons distinguer parmi elles les 2-catégories finiment biprésentables comme étant celles possédant les bicolimites pondérées - ou de façons équivalentes les bilimites pondérées - et qu'elles correspondent exactement aux catégories de pseudofoncteurs plats sur des petites 2-catégories avec limites finiment pondérées.

Nous prouvons par ailleurs des théorèmes de pseudofoncteurs bi-adjoints dans un contexte bi-accessible permettant de définir la bonne notion de morphismes de 2-catégories finiment présentables, et déduisons une dualité de Gabriel-Ulmer 2-dimensionelle.

Nous nous tournons ensuite sur les exemples motivant cette notion, parmi les doctrines du premier ordre. Nous prouvons tout d'abord que les catégories de pseudo-algèbres d'une 2-monades préservant les bicolimites bifiltrées forment une 2-catégorie finiment biprésentable. Ceci englobe en particulier le cas de Lex, la doctrines des petites catégories avec limites finies et foncteurs exacts à gauche. Les autres exemples sont capturés via le formalisme des “colimites lex” de Garner & Lack ; celui-ci repose sur une notion de “$\Phi$-exactitude” relativement à une classe $\Phi$ de poids finis (qui peut se comprendre comme une condition de cocomplétude dans Lex): nous appuyant sur le résultat précédent, nous montrons que les 2-catégories de catégories $\Phi$-exactes sont finiment biprésentables pour toute classe de poids finis: ainsi des doctrines Reg des catégories régulières, Ex des catégories exactes, Coh des catégories cohérentes, Adh des catégories adhésives, Ext$_\omega$ des catégories lextensives, Pretop$_\omega$ des prétopos finitaires…

Enfin, si le temps le permet, nous discuterons une façon plus concrète de prouver ces mêmes résultats via des méthodes d'injectivité où se manifestent plus intuitivement des manipulations d'une sorte de “2-logique cartesienne” à base de “prédicats 2-dimensionnels” impliquant des diagrammes de variables finis.

Cet exposé se basera sur le travail mené conjointement avec Ivan Di Liberti :

Higher categories, polygraphs and homotopy
Monday March 28, 2022, 2PM, séance en ligne :
Andrea Gagna (Czech Academy of Sciences) Fibrations de (∞, 2)-catégories

Dans cet exposé je vais introduire les ensembles simpliciaux à écailles comme cadre pour les (∞,2)-catégories, qui sont définies par des propriétés de relèvements qui encodent de manière combinatoire l'algèbre des 2-catégories et les cohérences homotopiques. Après, j'introduirai des fibrations entre (∞,2)-catégories qui ont pour but de classifier les foncteurs d'une petite (∞,2)-catégorie vers l'(∞,2)-catégorie des petites (∞, 2)-catégories, dans l'esprit de la correspondance de Grothendieck-Lurie. On donne des exemples basiques de telles fibrations, on en liste des jolies propriétés et on les compare avec des homologues enrichies. On conclut avec une sortie dans le monde de 2-limites dans ce cadre homotopique, qui se définissent et manipulent à l'aide des fibrations.

notez l'horaire inhabituel !

Higher categories, polygraphs and homotopy
Friday January 14, 2022, 2PM, *exceptionnellement en salle 3052*
Hugo Moeneclaey (IRIF) Monoidal models of type theory as notions of parametricity

Some models of type theory are parametric in the sense that every type comes with a canonical relation, and every term respects these. We proved that the forgetful functor:
Parametric models -> Models of type theory 

has a right adjoint, building cubical models for type theory.

Various notions of parametricity for various kind of models can be considered, for example with a predicate rather than a relation (realizability) or reflexive relations (internal parametricity). In this talk we will focus on how to build a right adjoint giving 'cubical models’ in all these situations.

To achieve this we will give a general axiomatisation, where a notion of parametricity will turn out to be a some kind of monoidal model. Then we will give examples fitting this framework, and sketch how to get the following as cubical models:

  1. Bicubical objects in a category.
  2. Categories internal to a lex category.
  3. Reedy fibrant cubical objects in a clan.

Séance en mode hybride. Participation à distance via le lien

Year 2021

Higher categories, polygraphs and homotopy
Friday December 10, 2021, 2PM, Salle 1007
Alain Prouté À la découverte des preuves mathématiques formelles

Dans cet exposé, je propose une méthode nouvelle pour introduire la notion de preuve mathématique formelle. Contrairement à ce qui est habituellement proposé, à savoir une introduction basée sur un postulat, comme par exemple le postulat de la correspondance de Curry-Howard, cette méthode ne suppose aucun postulat. Elle n'utilise que des faits que les mathématiciens, et en particulier les mathématiciens non logiciens, admettent sans discussion, parce que ce sont des mécanismes qu'ils utilisent tous les jours. Comme la méthode ne suppose aucune syntaxe a priori pour les preuves, la définition des preuves que je vais donner est un cadre général qui pourrait a priori accommoder différentes syntaxes de preuves. Toutefois on verra, qu'à condition de ne pas introduire de choses inutiles dans le langage, et au variations syntaxiques superficielle près, il n'y a essentiellement qu'un seul langage de preuve possible. On verra quelques exemples de preuves formelles. La méthode met aussi immédiatement en évidence l'existence d'un opérateur de choix et d'un opérateur de description. Ceci m'amènera aussi (si le temps imparti le permet) à discuter de l'axiome du choix et de son rapport au langage ainsi mis en évidence.

Higher categories, polygraphs and homotopy
Friday December 3, 2021, 2PM, Salle 1007
Guillaume Laplante-Anfossi (Université Sorbonne Paris-Nord) La diagonale des opéraèdres

La diagonale ensembliste d’un polytope a le défaut rédhibitoire de ne pas être cellulaire: son image n’est pas une union de cellules. Notre but sera ici de développer une théorie générale, basée sur la méthode introduite par N. Masuda, H. Thomas, A. Tonks et B. Vallette, afin de comprendre et de manipuler les approximations cellulaires de la diagonale d’un polytope quelconque. Cette théorie nous permettra d’attaquer le problème de l’approximation cellulaire de la diagonale des opéraèdres, une famille de polytopes allant des associaèdres aux permutoèdres, et qui code les opérades à homotopie près. Nous obtiendrons ainsi une formule explicite pour le produit tensoriel de deux telles opérades, aux propriétés combinatoires intéressantes.


Higher categories, polygraphs and homotopy
Friday November 26, 2021, 2PM, Salle 1007
Dimitri Ara (Université d“Aix-Marseille) Comparaison des nerfs pour les n-catégories strictes

Le foncteur nerf permet d'associer à toute petite catégorie un type d'homotopie, donnant lieu à une théorie de l'homotopie des petites catégories, développée par Quillen, Thomason et Grothendieck. Pour généraliser cette théorie aux catégories supérieures, on a besoin d'un analogue supérieur au foncteur nerf. Or il existe plein de tels foncteurs!

Le but de cet exposé, basé sur un article en collaboration avec Georges Maltsiniotis, sera d'expliquer des généralités sur la comparaison de foncteurs nerf et de montrer que pour les n-catégories strictes le nerf multi-simplicial, le nerf cellulaire et le nerf de Street sont tous équivalents.

Higher categories, polygraphs and homotopy
Friday November 5, 2021, 2PM, Salle 1007
Albert Burroni (IRIF) Les esquisses revisitées comme présentations équationnelles des algèbres graphiques (dans une perspective doctrinale)

Une courte première partie de cet exposé sera de nature épistémologique. Il s'agira de situer la question, existence et légitimité du problème : esquisses versus algèbres graphiques. L'intrusion de la structure de catégorie dans l'univers structuraliste de Bourbaki du siècle dernier est venue perturber cet univers au moins par deux aspects. Je ne suis pas concerné ici par celui qui parle des fondements. Le second, objet de cet exposé, est celui de la structure même des catégories et de leurs multiples dérivés. Deux conceptions de ces structures, géométriques et/ou algébriques, conduisent à certains clivages dans leurs traitements. Je rappellerai les définitions associées aux deux points de vue : 1) Les esquisses d'Ehresmann introduites en 1966, lesquelles ont fait l'objet de nombreux travaux par certains de ses élèves pendant plusieurs décennies. 2) Les algèbres graphiques introduites par moi en 1981 (voir lien ci-dessous). Je précise que la juste formule n'est pas d'opposer les esquisses aux algèbres graphiques, mais les esquisses aux théories algébriques graphiques (on est au niveaux des théories).

Higher categories, polygraphs and homotopy
Friday October 22, 2021, 2PM, Salle 1007
Antoine Allioux (IRIF) Structures supérieures cohérentes en théorie des types homotopiques

Travail mené conjointement avec Eric Finster et Matthieu Sozeau (

La théorie des types de Martin-Löf peut être vue comme une fondation des mathématiques. Il a été montré que certains de ses modèles validaient une interprétation homotopique des types, ce qui a motivé une nouvelle ligne de développement de celle-ci nommée théorie des types homotopiques.

Dans cette théorie, les types ne sont pas vus comme de simples ensembles car ils ont une structure d'infini-groupoïde non-triviale conférée par leurs types identité. D'où l'idée de formaliser des résultats d'algèbre supérieure en exploitant la structure supérieure des types. Néanmoins, décrire celle-ci de façon interne reste une question ouverte. C'est à dire que l'on peut énoncer des propositions concernant des infini-groupoïdes arbitraires mais que l'on ne sait pas construire une large classe d'infini-groupoïdes, en particulier ceux dont la structure supérieure n'est pas triviale ou tronquée à partir d'une certaine dimension.

Nous proposons une approche consistant à étendre la théorie des types avec un univers de monades polynomiales satisfaisant leurs lois de façon définitionnelle. Cela nous permet de présenter les types et leur structure supérieure, et ainsi d'internaliser un certain nombre de résultats dont le fait que les types sont des infini-groupoïdes.

Higher categories, polygraphs and homotopy
Friday October 1, 2021, 2PM, Salle 1007
El Mehdi Cherradi (IRIF) Dérivateurs de Quillen et doubles catégories

Étant donnée une catégorie avec une notion d'homotopie, par exemple une catégorie relative, la notion de dérivateur introduite par Grothendieck permet de décrire les catégories de diagrammes à homotopie près, et les relations fonctorielles qu'elles entretiennent.

Dans cet exposé, nous étudierons comment le prédérivateur associé à une telle catégorie relative se restreint en un objet simplicial dans la catégorie CAT des catégories (non nécessairement petites). Cet objet simplicial peut être vu comme un “nerf homotopique” qui décrit les chemins de longueurs n dans la catégorie d'origine, vus à homotopie près.

Partant de ces observations, nous montrerons que dans le cas d'une catégorie de modèle, l'objet simplicial satisfait une condition de Segal, et définit pour cette raison une double catégorie. Cette double catégorie peut être vue comme combinant en une seule structure la catégorie de modèle d'origine (horizontalement) et sa catégorie homotopique (verticalement).

Nous montrons aussi que la construction précédente est compatible avec la structure de dérivateur établie par Cisinski pour un prédérivateur associé à une catégorie de modèle : on obtient ainsi un nouveau dérivateur prenant ses valeurs dans la catégorie DblCAT des doubles catégories plutôt que dans CAT.

Higher categories, polygraphs and homotopy
Friday June 4, 2021, 2PM, Salle 1007
Léonard Guetta (IRIF) Les préfaisceaux en groupoïdes comme modèles de types d'homotopie

En théorie de l'homotopie, l'omniprésence de la catégorie des ensembles simpliciaux semble lui donner un rôle particulier. Parmi les raisons de sa popularité, on peut citer au moins trois propriétés essentielles : (1) Les ensembles simpliciaux modélisent les types d'homotopie (Milnor), (2) Les groupes internes aux ensembles simpliciaux modélisent les types d'homotopie pointés connexes (Kan), (3) Les groupes abéliens internes aux ensembles simpliciaux modélisent les “types d'homologie”, autrement dit la théorie de l'homotopie des complexes de chaînes en degrés positifs (Dold-Kan-Puppe).

En fait, la propriété (2) admet même la généralisation suivante due a Joyal et Tierney :

(4) Les groupoïdes internes aux ensembles simpliciaux modélisent les types d'homotopie.

Il est alors naturel de se demander s'il existe d'autres catégories de préfaisceaux qui admettent les mêmes propriétés, et qui sont donc, en un certain sens, aussi “bonnes” que la catégorie des ensembles simpliciaux pour faire de la théorie de l'homotopie. Dans Pursuing Stacks, Grothendieck développe la théorie des catégories tests, qui sont, très grossièrement parlant, les petites catégories A tels que les préfaisceaux sur A satisfont à l'analogue de la propriété (1) énoncée plus haut. Le constat est clair : la catégorie des simplexes est loin d'être la seule à satisfaire cette propriété et les catégories tests sont légion.

Dans cet exposé, je présenterai mes travaux récents portant sur la théorie des “catégories tests au sens des groupoïdes”, variation de la théorie des catégories tests de Grothendieck et qui sont, grossièrement parlant, les petites catégories A tels que les préfaisceaux sur A satisfont à l'analogue de la propriété (4) énoncée plus haut. Un des résultats importants que je présenterai est :

Une (petite) catégorie est test si et seulement si elle est test au sens des groupoïdes.

Outre le fait qu'il permet de déduire de nombreux nouveaux modèles des types d'homotopie, ce résultat non trivial permet de renforcer, une fois de plus, la pertinence de la notion de catégorie test.

Si le temps me le permet, je terminerai l'exposé par des généralisations conjecturales de cette théorie des “catégories test au sens des groupoïdes”, qui visent notamment à remplacer les groupoïdes par des n-groupoïdes (faibles).

Higher categories, polygraphs and homotopy
Friday March 19, 2021, 2PM,
Chaitanya Leena-Subramaniam (IRIF) Structures algébriques décrites par les théories à types dépendants

Une catégorie localement présentable peut parfois être décrite comme la catégorie des modèles (dans Ens) d'une théorie algébrique à types (ou sortes) dépendants. Nous en avons vu un exemple (présenté par T. Benjamin) lors d'une séance précédente : la catégorie des omega-catégories faibles du cohérateur de Batanin-Leinster.

Il est naturel de se demander quelles structures algébriques admettent une telle description et si l'on peut les reconnaître « dans la nature ». Dans cet exposé je répondrai à cette question.

Plus précisément, je montrerai que :

1. Les signatures de types dépendants correspondent exactement aux catégories directes localement finies. (Cette description est due à Makkai et porte le nom de “simple category” dans ses travaux sur les FOLDS.)

2. Si C est une catégorie directe localement finie (telle que celles des globes, des semi-simplexes, ou des opétopes), alors les contextes de variables typées par C sont exactement les complexes cellulaires finis dans [C^op, Ens]. (N.B. : La catégorie C étant directe, les préfaisceaux sur C admettent un modèle cellulaire donné par les inclusions de bords de représentables.)

3. La catégorie des « théories algébriques typées par une signature C » est équivalente à celle des monades finitaires sur [C^op, Ens].

4. La catégorie des modèles dans Ens d'une théorie algébrique typée par C est équivalente à la catégorie des algèbres de la monade finitaire correspondante.

On en déduit (parmi d'autres) les exemples des théories algébriques à types dépendants des oméga-catégories et oméga-groupoïdes (strictes et faibles), des opérades colorées (planaires), des ensembles opétopiques, et des combinades (sur les arbres planaires) de Loday. Je les expliquerai.

5. Enfin, je montrerai un résultat un peu surprenant : les théories algébriques à types dépendants sont aussi expressives que les théories essentiellement algébriques ou les esquisses projectives. Autrement dit, toute catégorie localement finiment présentable est la catégorie des modèles dans Ens d'une théorie algébrique à types dépendants.

Ce dernier peut aussi être vu comme conséquence de la version non-homotopique d'un résultat de Cisinski permettant de calculer les extensions de Kan à droite homotopique des préfaisceaux à valeurs dans une catégorie de modèles par passage aux préfaisceaux sur des catégories directes (localement finies).

enregistrement :

Higher categories, polygraphs and homotopy
Friday March 12, 2021, 2PM,
Félix Loubaton (Université Côte d'Azur) Conditions de Kan sur les nerfs des oméga-catégories

Il est bien connu que le nerf d'une catégorie C est toujours une quasi-catégorie, et qu'il est un complexe de Kan si et seulement si C est un groupoïde. Le foncteur nerf de Street, entre la catégorie des petites oméga-catégories et celle des ensembles simpliciaux peut être vu comme une généralisation du nerf catégorique. Il est alors naturel de se demander si on peut, de façon analogue au cas catégorique, caractériser les oméga-catégories dont le nerf de Street est un complexe de Kan (resp. une quasi-catégorie). La réponse est affirmative : cela correspond au oméga-catégories dont les n-cellules sont faiblement inversibles pour n>0 (resp. n>1).

Dans cet exposé, après des rappels sur les oméga-catégories, nous présenterons une preuve de ce fait. Si le temps le permet, nous présenterons une généralisation aux ensembles compliciaux.

Cet exposé est basé sur le papier suivant :

enregistrement :

Higher categories, polygraphs and homotopy
Friday February 12, 2021, 2PM,
Thibaut Benjamin (LIX) CaTT : Une theorie des types qui decrit les omega-categories faibles

Les omega-catégories faibles, comme toutes les structures supérieures, sont délicates a définir et a manipuler. La raison est qu'elles ont de la structure dans toutes les dimensions, et que cette structure est cohérente: pour chaque dimension, les bonnes propriétés vérifiées par la structure dans cette dimension sont encodées par des éléments de dimension supérieure. La conséquence est qu'au fur et à mesure que l'on monte en dimension, les éléments présents deviennent de plus en plus riches et complexes a décrire. Ainsi, les définitions possibles de ces structures s'appuient sur des schémas d'axiomes, permettant de générer l'infinité d'opérations et de cohérences en toute dimensions, et ces schémas d'axiomes sont eux-mêmes encodés dans des structures algébriques adéquates, comme une opérade globulaire (définition due a Batanin et Leinster) ou une catégorie avec certaines colimites (définition due a Grothendieck et Maltsiniotis). Plus récemment, Finster et Mimram ont proposé une définition des omega-catégories faibles en encodant ces schémas d'axiomes dans une théorie des types, CaTT. Dans cet exposé, je vais présenter la theorie CaTT et m'appuyer sur cette formulation pour présenter formellement les omega-categories faibles. Je vais ensuite faire une démonstration d'un assistant de preuve pour les oméga-categories faibles que j'ai implementé en m'appuyant sur cette théorie des types et discuter des possibilités de cet outil, ainsi que des améliorations que j'y ai apportées. Je vais finalement esquisser une comparaison entre CaTT et la définition de Grothendieck-Maltsiniotis des omega-catégories faibles.

Year 2020

Higher categories, polygraphs and homotopy
Friday May 8, 2020, 2PM, * à distance *
Cameron Calk (LIX) Coherent confluence in modal n-Kleene algebras

In this talk, I will discuss recent work with Philippe Malbos, Eric Goubault and Georg Struth, concerning the algebraic formalisation of coherence and confluence. In the context of abstract rewriting systems (ARSs), the Church-Rosser theorem states that every branching can be completed with a confluence if, and only if, every zig-zag can be completed with a confluence. The relational formulation of this theorem has been abstracted to the setting of Kleene algebra, in which a proof is accomplished by means of a formal calculation. Furthermore, rewriting properties may be defined in Kleene algebra using simple inequalities, and a rich modal structure, defined via domain and codomain operators, has been developed. Polygraphs have equally been applied to ARSs. Higher dimensional cells are used to define coherence properties of ARSs and reduction/normalisation strategies. These constructions are linked to the notion of cofibrant replacement in the folk model structure on omega-categories, in the sense that a coherent presentation of a category by a polygraph constitutes its cofibrant replacement. A coherent formulation of the Church-Rosser theorem is expressed in the language of polygraphs. We combine these two approaches by introducing the structure of (globular) modal n-Kleene algebra, thereby providing a natural setting for the formalisation of coherent confluence. We formulate and prove both the Church-Rosser theorem and Newman's lemma in this setting, and provide an explicit link to polygraphs: the power set of the set of $n$-cells of the free category generated by a polygraph is a globular modal $n$-Kleene algebra with source, target and composition maps lifted to the set-level. In the talk, I will present the main definitions and examples, and briefly sketch a proof of the coherent Church-Rosser theorem in globular modal n-Kleene algebras.

Higher categories, polygraphs and homotopy
Friday April 17, 2020, 2PM, * à distance *
Chaitanya Leena-Subramaniam (IRIF) The small object argument for unique factorisation systems and the “plus” construction for sheaves (j.w.w. Mathieu Anel)

We work in the setting of ∞-categories and use the terminology “category” = “∞-category” = “(∞,1)-category”, “topos” = “∞-topos”, “presheaf” = “presheaf of ∞-groupoids”. All our results hold for 1-categories and 1-topoi as well.

The small object argument of Quillen is a well-known construction of the weak factorisation system generated “on the left” by a small set of arrows of a category.

We recall a variant of the small object argument, essentially due to Kelly, that constructs the unique factorisation system (^\bot(W^\bot), W^\bot) generated by a small diagram W of morphisms of a locally presentable category C. Our main result shows that, given sufficient conditions on W (called a “pre-modulator”), Kelly's construction simplifies so that the unique factorisation of any morphism is given by iterating a “plus construction” generalising the one known from sheafification. Further, any small diagram can be replaced with a pre-modulator that generates the same unique factorisation system. Thus we show that every accessible reflective localisation of a locally presentable category can be calculated as a transfinite iteration of a plus construction. The classical plus construction for Grothendieck sites is a particular case, given by the pre-modulator (in fact a lex modulator) corresponding to the Grothendieck topology (seen as a diagram of sub-representables).

We also define “modulators” (resp. “lex modulators”) and prove that their corresponding unique factorisation systems are modalities (resp. lex modalities). It makes sense to see lex modulators as the correct generalisation of the notion of Grothendieck topology from 1-categories to ∞-categories, since every left-exact localisation (topological or not) of an ∞-topos can be obtained from a lex modulator. We show moreover that the plus construction associated to any lex modulator on an ∞-topos converges after (n+2) iterations when applied to an n-truncated object. This explains why the usual plus construction for 1-topoi converges after 2 iterations. The talk will present the main results and examples, without going into much detail of the demonstrations.

Higher categories, polygraphs and homotopy
Friday February 28, 2020, 2PM, Salle 1007
Sebastian Posur (Universität Siegen) Methods of constructive category theory

Categorical abstraction is a powerful organizing principle in computer algebra. In this talk, we explain the concept of constructive category theory and how we implement this concept in our software project CAP-Categories, algorithms, programming. In CAP it is possible to implement higher algorithms and data structures using basic categorical operations as primitives, which in turn often rely on classical algorithms in computer algebra like the computation of Gröbner bases. As an example, we show how our categorical framework can be used for computing with finitely presented functors.

Higher categories, polygraphs and homotopy
Thursday February 27, 2020, 2PM, Salle 1012
Michael Batanin (IHES) Comparing symmetric operads and operadic categories

The notion of operadic category appeared in the work of Batanin and Markl as a tool for working with various operad like structures. Each operadic category O has an associated category of O-operads with values in an arbitrary symmetric monoidal category. Operadic categories and operadic functors form a category.

In my talk I will show that the category of symmetric operads in Set (variation of colours is allowed) is a reflective subcategory of the category of operadic categories. The inclusion is given by (operadic) Grothendieck construction and the reflection is given by evaluation of the left Kan extension along arity functor on the terminal operad. Thus the notion of operadic category can be considered as a flexible extension of the notion of symmetric operad.

Moreover, there is yet another functor from operadic categories to symmetric operads which sends an operadic category O to a symmetric operad in Set whose algebras are exactly O-operads. These three functors (Grothendieck construction, its left adjoint and free operad functor) fit in a nice picture with a universal property. In particular, they various composites generate the Baez-Dolan +-constructions for both symmetric operads and operadic categories.

*Attention : date et salle inhabituelles !*

Higher categories, polygraphs and homotopy
Friday February 7, 2020, 2PM, Salle 1007
Nima Rasekh (EPFL/IHES) Fibrations for Segal Spaces

An (oo,1)-category is a weak notion of a category where composition and associativity is only defined up to higher coherences. For that reason it is often impossible to directly define functors and we thus use fibrations instead.

For quasi-categories, a popular model of (oo,1)-categories, fibrations have been studied carefully by Joyal and Lurie and are commonly used in all kinds of categorical constructions.

In this talk we define and study left fibrations for another model of (oo,1)-categories, namely complete Segal spaces. We will show that these fibrations come with a model structure and that we can characterize the fibrant objects and the equivalences of the model structure, which allows us to prove many strong results about such fibrations without ever translating to functors.

If time permits we will discuss one particular strength of this approach to the theory of fibrations, namely how it can be generalized to fibrations for the (oo,n)-categorical analogue of complete Segal spaces: n-fold Segal spaces.

Higher categories, polygraphs and homotopy
Friday January 17, 2020, 2PM, Salle 1007
Johan Leray (LAGA-Université Paris 13) La propérade encodant les algèbres double Poisson est de Koszul

Les algèbres double Poisson sont une version non commutative des algèbre de Poisson et apparaissent aujourd'hui dans de nombreux domaines mathématiques. Afin de déterminer une version à homotopie près de cette structure algébrique, il est nécessaire de déterminer une résolution cofibrante de la propérade qui l'encode. Après avoir rappeler la notion de propérade, je présenterai la stratégie afin de démontrer la koszulité de cette propérade. Celle-ci fait notamment intervenir un nouveau type de monoïde, appelé protopérade, qui permet de ramener ce problème difficile de koszulité à un autre, plus simple, permettant ainsi d'utiliser des arguments de réécriture pour conclure.

Year 2019

Higher categories, polygraphs and homotopy
Friday December 20, 2019, 2PM, Salle 1007
Simon Henry (Université d'Ottawa) Les polygraphes homotopiques sont des préfaisceaux

On peut définir les polygraphes dans des cadres assez généraux. Par exemple si M est une monade sur une catégorie de préfaisceaux sur une catégorie I dirigée, on peut définir une notion de M-polygraphe. Si M a de bonnes propriétés (fortement cartésienne) alors la catégorie des M-polygraphes a des propriétés très similaires à la catégorie des polygraphes ordinaires.

Dans cet exposé on va étudier une version infini-catégorique de cette construction. On partira d'une monade M fortement cartésienne sur un infini topos, et on construira une infini-catégorie de M-polygraphes. Le cas de la monades infini-catégories strictes agissant sur la catégorie des espaces globulaires donne une version homotopique des polygraphes ordinaires.

On montrera que l'infini-catégorie M-polygraphes a toujours de très bonnes propriétés, qu'on aimerait avoir pour les polygraphes ordinaires mais qui échouent en dimension >2. En particulier les M-polygraphes forment un infini-topos (et si M agit sur une catégorie de préfaisceaux, les M-polygraphes forment une infini-catégorie de préfaisceaux). Si le temps le permet, on montrera comment ces polygraphes homotopiques sont reliés aux polygraphes ordinaires et permettent de déduire des résultats sur les polygraphes ordinaires.

Higher categories, polygraphs and homotopy
Friday December 13, 2019, 2PM, Salle 1007
Chaitanya Leena-Subramaniam (IRIF) Opetopic algebras II: Homotopy-coherent opetopic algebras

Higher categories, polygraphs and homotopy
Friday November 29, 2019, 2PM, Salle 1007
Cédric Ho Thanh (IRIF) Opetopic algebras I: Algebraic structures on opetopic sets

Higher categories, polygraphs and homotopy
Friday November 22, 2019, 2PM, Salle 1007
Maxime Lucas (INRIA Nantes) La structure de catégorie de modèles folk sur omega-Cat est monoïdale

Higher categories, polygraphs and homotopy
Friday November 15, 2019, 2PM, Salle 1007
Juan Pablo Vigneaux (MPI MiS Leipzig) Une caractérisation homologique de l'entropie différentielle

Il y a plusieurs caractérisations algébriques (dites “axiomatiques”) de l'entropie discrète de Shannon. Je vais présenter ici une caractérisation analogue pour l'entropie différentielle, qui apparaît dans la théorie de compression des signaux continus: le cadre utilisé est la “cohomologie de l'information”, associé aux préfaisceaux sur certaines structures combinatoires. Si le temps le permet, je vais présenter d'autres théories cohomologiques des faisceaux très proches, définies sur les graphes (Friedman) et les complexes simpliciaux (Abramsky et al.), qui correspondent aussi à la cohomologie des topos.

Higher categories, polygraphs and homotopy
Friday October 18, 2019, 2PM, Salle 1007
Léonard Guetta (IRIF) Colimites homotopiques et tranches

Un résumé de l'exposé est accessible à l'adresse :

Higher categories, polygraphs and homotopy
Friday October 4, 2019, 2PM, Salle 1007
Amar Hadzihasanovic (RIMS Kyoto) Representable diagrammatic sets: a model of weak omega-categories

I will talk about a model of weak omega-categories built around the combinatorics of pasting diagrams. The goal is to have a framework where higher-dimensional theories explicitly presented by generators (or higher-dimensional rewrite systems) can be interpreted directly in general higher categories. The talk is based on arXiv preprint 1909.07639.

Higher categories, polygraphs and homotopy
Friday June 21, 2019, 2PM, Salle 1007
Alain Prouté Qu'est-ce qu'un ensemble ?

Si, il y a 10.000 ans, il y avait un mot pour désigner un troupeau de moutons, ce mot voulait aussi dire «ensemble», même si cette notion d'ensemble était moins abstraite que celle que Bolzano, Dedekind et Cantor introduisirent à la fin du XIXe siècle. On pourrait croire qu'après la théorie des ensembles de Zermelo et Fraenkel, la question de savoir ce qu'est un ensemble était close. Ce n'est pas le cas comme le remarque par exemple Quine, auteur d'une théorie alternative, qui dit dans les années 60 que la question est toujours ouverte. Une nouvelle impulsion sera donnée par Lawvere avec sa théorie axiomatique de la catégorie des ensembles, et surtout par Lawvere et Tierney avec la notion de topos élémentaire. Cette dernière notion inspirera Volger, puis Lambek, qui définira la notion de «dogme». J'ai rebaptisé leur théorie en «théorie des ensembles de Volger-Lambek». J'en donnerai une description et j'expliquerai pourquoi elle est, à condition qu'elle soit un peu généralisée, la bonne théorie de formalisation non seulement des ensembles, mais de toute la mathématique telle que nous la pratiquons aujourd'hui.

Higher categories, polygraphs and homotopy
Friday May 24, 2019, 2PM, Salle 1007 - Séance co-organisée avec le groupe de travail “Théorie des types et réalisabilité”
Hugo Moeneclaey (ENS Paris-Saclay) Monoids up to Coherent Homotopy in Two-Level Type Theory

When defining a monoid structure on an arbitrary type in HoTT, one should require a multiplication that is not only homotopy-associative, but also has an infinite tower of higher homotopies. For example in dimension two one should have a condition similar to Mac Lane’s pentagon for monoidal categories. We call such a monoid a monoid up to coherent homotopy. The goal of my internship in Stockholm was to formalize them in Agda. It is well-known that infinite towers of homotopies are hard to handle in plain HoTT, so we postulate a variant of two-level type theory, with a strict equality and an interval type. Then we adapt the set-theoretical treatment of monoids up to coherent homotopy using operads as presented by Clemens Berger and Ieke Moerdijk [1,2].

Our main results are: (a) Monoids up to coherent homotopy are invariant under homotopy equivalence (b) Loop spaces are monoids up to coherent homotopy.

In this talk I will present the classical theory of monoids up to coherent homotopy, and indicates how two-level type theory can be used to formalize it.


1. Axiomatic homotopy theory for operads (

2. The Boardman-Vogt resolution of operads in monoidal model categories (

Séance co-organisée avec le groupe de travail “Théorie des types et réalisabilité”

Higher categories, polygraphs and homotopy
Friday May 10, 2019, 2PM, Salle 1007
Pierre-Louis Curien (IRIF) Surfaces et preuves

Travail en commun avec Djordje Baralić, Marina Milićević, Jovana Obradović, Zoran Petrić, Mladen Zekić et Rade Zivaljević

Une situation de Menelaüs est la donnée d'un triangle (non dégénéré) et de points pris sur les trois lignes supportant le triangle qui sont alignés. On peut voir ces trois points comme des témoins des 1-cellules du triangle. Prenons maintenant un ensemble simplicial, satisfaisant certaines conditions garantissant notamment que sa réalisation est une 2-variété. Prenons une interprétation de toutes les 0-cellules et 1-cellules par des points dans le plan (euclidien ou projectif). Alors la présence d'une situation de Menelaüs sur tous les triangles de l'interprétation sauf un induit une situation de Menelaus sur le dernier. C'est cette observation, dûe à Jürgen Richter-Gebert, qui nous a conduit à introduire un syst!me logique (plus précisément un calcul des séquents) “cyclique”, ainsi qu'une opérade cyclique dite de Menalaüs, dont nous avons cru un bon moment qu'elle était libre, jusqu'à trouver un contre-exemple. Nous en donnons une présentation par générateurs et relations.

Higher categories, polygraphs and homotopy
Friday April 5, 2019, 2PM, Salle 1007
Simon Henry (Masaryk University, Brno) Nouvelles constructions de catégories de modèles

Je présenterai rapidement des affaiblissements de la notion de “catégorie de modèles de Quillen” (les semi catégories de modèle à gauche et à droite et les structures de modèles faibles) et je parlerai de plusieurs (nouveaux) théorèmes permettant de construire facilement des catégories de modèles. Notamment, j'espère présenter des solutions (au moins dans le cadres des semi-catégorie de modèles) à deux vieux problèmes en théorie des catégorie de modèles: l'existence des structures de modèles déterminés à gauche (et plus généralement: étendre la théorie des structures de modèles de Cisinski à toutes les catégorie présentable) et, si le temps le permet, la construction d'une “catégorie de modèle des catégories de modèles”.

Higher categories, polygraphs and homotopy
Friday March 15, 2019, 2PM, Salle 1007
Jovana Obradovic (Institute of Mathematics, Czech Academy of Sciences) Combinatorial homotopy theory for cyclic operads

This talk is a sequel of the talk I gave on November 30th 2018, when I introduced an explicit combinatorial characterization of the minimal model of the coloured operad encoding non-symmetric operads. Having identified the family of polytopes whose elements display the homotopies relating different ways of composing the nodes of rooted trees, a question of characterizing homotopy polytopes of more general graphs arises. In this talk, I will answer that question for unrooted trees by introducing a combinatorial resolution of the coloured operad encoding non-symmetric cyclic operads. The algebras over this resolution yield a notion of strongly homotopy cyclic operads for which both the relations for the partial composition operations, and the relation for the action of cyclic permutations that permutes the factors of the composition, are coherently relaxed up to homotopy. The operations of this resolution are faces of polytopes that can be characterized as Cartesian products of n-dimensional operatic polytopes and (n+1)-dimensional hypercubes.

Higher categories, polygraphs and homotopy
Friday March 8, 2019, 2PM, Salle 1007
Pedro Tamaroff (Trinity College Dublin) Minimal models for monomial algebras

In 1985, David Anick introduced a combinatorial construction of chains which can be used to compute various homological invariants of an associative algebra from a good presentation of it by generators and relations. In particular, for algebras with monomial relations, his construction produces those invariants directly.

In this talk, I will explain how to compute a rich algebraic structure on Anick chains leading to the explicit formula for a minimal dg model for any monomial algebra. This is a replacement of an algebra by a differential graded algebra with the same homological properties. This computation relies on the algebraic discrete Morse theory of Jöllenbeck, Welker and Sköldberg and on homotopy transfer formulas; those are formulas perfectly suited for homological computations where the underlying chain complexes are of combinatorial nature. Prior knowledge of these techniques is not required, as they will be explained along the way.

Our work suggests a conjectural answer to obtain possibly non-minimal (yet small) models for algebras with a Groebner basis that I will also discuss.

The talk is based on the paper available at

Higher categories, polygraphs and homotopy
Friday February 22, 2019, 2PM, Salle 1007
Cédric Ho Thanh (IRIF) The equivalence between many-to-one polygraphs and opetopic sets

Higher categories, polygraphs and homotopy
Friday February 15, 2019, 2PM, Salle 1007
Chaitanya Leena-Subramaniam (IRIF) Un lien entre la construction de Boardman-Vogt pour les opérades et l’argument du petit objet pour les systèmes de factorisation orthogonale (II)

Cet exposé est la suite de celui du 11 janvier ; cependant, il sera accessible aux nouveaux auditeurs.

L’exposé commencera avec des rappels sur les monades à arités et leurs “théories de Lawvere généralisées” et expliquera le rôle de l’argument du petit objet (pour les systèmes de factorisation orthogonale) dans leur description. Ces notions se généralisent aux \infty-catégories ((\infty,1)-catégories), et j’essaierai de les décrire dans le cadre des \infty-catégories localement présentables présentées par des catégories de modèles simpliciales.

L’exposé continuera avec l’exemple de la monade (à arités) de Set-opérade (symétrique colorée) libre sur une Set-collection, dont la généralisation exhibe l’\infty-catégorie des \infty-opérades comme une \infty-catégorie d’algèbres pour la même “théorie de Lawvere généralisée”.

Higher categories, polygraphs and homotopy
Friday February 8, 2019, 2PM, Salle 1007
Yves Guiraud (IRIF) Résolutions polygraphiques dans les algèbres différentielles graduées

Higher categories, polygraphs and homotopy
Friday February 1, 2019, 2PM, Salle 1007
Rafaël Bocquet (ENS) Morphismes conservatifs dans les catégories des modèles de théories algébriques généralisées

Hofmann a prouvé en 1995 un résultat de conservativité comparant l'axiome d'unicité des preuves d'égalité et les types identité extensionnels en théorie des types. Je vais présenter une généralisation de ce résultat dans le contexte plus général des théories algébriques généralisées. Un système de factorisation (cofibrations, fibrations triviales) est défini sur la catégorie des modèles d'une théorie algébrique généralisée, dont les fibrations triviales sont par exemple les morphismes conservatifs entre modèles de théories des types, les isofibrations surjectives sur les objets dans Cat ou les fibrations triviales de la structure de modèle folk sur omega-Cat. Dans ce cadre, une généralisation du théorème de Hofmann se déduit d'une caractérisation des fibrations triviales comme les quotients par une certaine classe de congruences.

Higher categories, polygraphs and homotopy
Friday January 18, 2019, 2PM, Salle 1007
Benjamin Dupont (Université de Lyon) Cohérence modulo et doubles groupoïdes

Higher categories, polygraphs and homotopy
Friday January 18, 2019, 10AM, 3052
Amar Hadzihasanovic (RIMS Kyoto University) Charted omega-categories

A charted omega-category is like a strict omega-category, but instead of a globular set, it has an underlying regular polygraph: its cells have more complex pasting diagrams “charted” on their boundary. Several features of omega-categories generalise nicely, including joins and the monoidal biclosed structure of lax Gray products. I will detail some of the combinatorics involved, going deeper into the theory of globular posets than in my talk last July (which is not a prerequisite).

Higher categories, polygraphs and homotopy
Friday January 11, 2019, 2PM, Salle 1007
Chaitanya Leena-Subramaniam (IRIF) Relating the W-construction for operads to the small object argument for factorisation systems

The first part of the talk will be devoted to showing that Moerdijk-Weiss’s category of dendrices \Omega is a Lawvere theory with arities for the free-operad monad on coloured symmetric Set-valued collections. This demonstration is due to J. Kock, following Weber, and generalises the known example of the category \Delta of simplices as a Lawvere theory with arities for the free-category monad on graphs.

If time permits, the second part will try to generalise this setting to simplicial operads and simplicial (i.e. sSet-enriched) model categories by replacing Set with the category sSet of simplicial sets, following Moerdijk-Weiss and Cisinski-Moerdijk.

The underlying theme is a variant of the small object argument that produces orthogonal factorisation systems (i.e. whose left and right maps lift uniquely against each other). This variant has been presented in a previous talk by M. Anel, and its generalisation to simplicial model categories is left Bousfield localisation.

Year 2018

Higher categories, polygraphs and homotopy
Friday December 14, 2018, 2PM, Salle 1007
Cameron Calk (ENS Lyon) L'homotopie dirigée et l'inversion temporelle

Higher categories, polygraphs and homotopy
Friday November 30, 2018, 2PM, Salle 1007
Jovana Obradovic (Université Charles, Prague) Combinatorial homotopy theory for operads

We introduce an explicit combinatorial characterization of the minimal model for the coloured operad encoding non-symmetric operads, whose structure generalizes the structure of Stasheff's topological $A_{\infty}$-operad.

Higher categories, polygraphs and homotopy
Friday October 19, 2018, 2PM, Salle 1007
Muriel Livernet (IMJ) Suites spectrales et équivalences faibles

Depuis leur introduction par Leray dans les années 50 les suites spectrales sont devenues essentielles dans beaucoup de domaines mathématiques comme outil de calculs homologiques et homotopiques. Parmi les sources importantes de suites spectrales on trouve les complexes filtrés et les bicomplexes. On introduit pour chacune de ces catégories la notion de E_r-quasi-isomorphisme, liée à la r-ième page des suites spectrales associées aux objets considérés. On montrera dans cet exposé, une fois toutes les notions utiles définies (y compris les structures de catégorie modèles) que les catégories des complexes filtrés et des bicomplexes admettent des structures de catégorie modèle au sens de Quillen, où les équivalences faibles sont les E_r-quasi-isomorphismes.

Ceci est un travail en commun avec: Joana Cirici, Daniela Egas-Santander et Sarah Whitehouse.

Higher categories, polygraphs and homotopy
Friday October 5, 2018, 2PM, Salle 1007
Eric Finster (IRIF) Vers l'algèbre universelle supérieure dans la théorie des types dépendants

Higher categories, polygraphs and homotopy
Friday September 28, 2018, 2PM, Salle 1007
Juan Pablo Vigneaux (IMJ-PRG) Une introduction à la topologie de l'information

Higher categories, polygraphs and homotopy
Thursday July 5, 2018, 2PM, Salle 1002
Amar Hadzihasanovic (RIMS Kyoto University) Regular polygraphs and semi-strictification of higher categories

A regular polygraph is one whose cells have k-dimensional boundaries “shaped as k-dimensional balls”, via a suitable geometric realisation. I will describe a combinatorial approach, where regular polygraphs are defined as presheaves on a shape category, and subsequently proved to form a full subcategory of the category of polygraphs. I will also show how several operations and constructions on polygraphs – such as lax Gray products and joins – admit a sleek definition in this setting.

I will then give a non-algebraic, fully weak definition of higher category, as a regular polygraph satisfying a representability property, and sketch a complementary algebraic, semi-strict definition. Finally, I will sketch how the two are combined in a semi-strictification construction, where semi-strictness should be read in the sense of “Simpson's conjecture for regular compositions”, as in the earlier seminar entry by Simon Henry.

The programme in the second part of the talk has been fully developed in dimension 2 (arXiv:1803.06086). The first part is the subject of a paper that I will publish or circulate before the talk.

Attention : changement de jour et de salle !

Higher categories, polygraphs and homotopy
Friday May 25, 2018, 2PM, Salle 1007
Martin Szyld (Université de Buenos Aires) The homotopy relation in a category with weak equivalences

I will present the results of the article (arXiv:1804.04244) which deals with the classical construction of the homotopy category of a model category (which is done by performing a quotient of the arrows by the homotopy relation) in the context of categories with weak equivalences. By studying this situation in an abstract context, one can define a relation of homotopy “only with respect to the weak equivalences” which yields the desired localization and coincides with the classical one for model categories. As it is usually the case, the proofs of these results, which consider only a family of arrows instead of three, become simpler. In particular, they allowed a generalization to bicategories in a current work with E. Descotte and E. Dubuc, which I will present too if time permits.

Higher categories, polygraphs and homotopy
Friday May 4, 2018, 2PM, Salle 1007
Simon Henry (Université Masaryk, Brno) Polygraphes réguliers et une preuve de la conjecture de Simpson pour les compositions régulières

La conjecture de Simpson affirme (informellement) que tout infini groupoïde (ou même infini catégorie) faible est équivalent à un dont les compositions, lois d'associativités, et lois d'échanges sont strictes, et seules les lois 'd'unités' (et donc aussi d'inverses) sont faibles. La conjecture est relativement vague et laisse de la place à l'interprétation, aussi bien sur la liste précise des opérations que l'ont veut rendre strictes, que sur la façon dont les “unités faibles” sont définies.

Dans l'exposé j'esquisserai la première preuve d'une forme de cette conjecture : celle-ci s'applique aux infinis groupoïdes, et strictifie les compositions dites 'régulières' (celles dont le diagramme est topologiquement une boule). Ce type d'opérations est suffisant pour engendrer toutes les opérations et cohérences attendues dans un infini groupoïde faible, dès qu'on lui ajoute des unités faibles et des inverses faibles. C'est donc une réponse satisfaisante à la conjecture d'origine, mais il existe encore des formes plus fortes de la conjecture non démontrées pour l'instant.

La démonstration repose en très grande partie sur des résultats nouveaux en théorie des polygraphes et sur d’excellentes propriétés d'une certaine classe des polygraphes dit “réguliers”. La plus grande partie de l'exposé sera concentrée sur ces aspects 'polygraphiques'.

Note: Il s'agit de la suite de mon exposé de Septembre “Les polygraphes non-unitaires et la conjecture de Simpson”, mais je ferai tous les rappels nécessaires.

Higher categories, polygraphs and homotopy
Friday April 6, 2018, 2PM, Salle 1007
Antonin Delpeuch (Oxford) Décider l'égalité de diagrammes de cordes

On propose une stratégie de réécriture pour obtenir des formes normales de diagrammes de cordes dans une catégorie monoïdale libre. On obtient une borne polynomiale sur la longueur maximale des réductions et on décrit un algorithme pour calculer les formes normales obtenues plus efficacement. Cela permet de décider l'égalité de diagrammes en temps quadratique. Une application possible serait d'implémenter l'algorithme dans Globular pour automatiser des étapes répétitives dans des preuves.

Higher categories, polygraphs and homotopy
Friday March 16, 2018, 2PM, Salle 1007
Léonard Guetta (IRIF) Non-universalité des colimites dans la catégorie des infini-catégories strictes

La catégorie des infini-catégories strictes n'est pas un topos. Cela se manifeste notamment par le fait que les colimites ne sont pas universelles, c'est-à-dire ne sont pas préservées par tiré-en-arrière (i.e. “pullback”) le long de n'importe quelle flèche. De manière équivalente, cela signifie qu'il existe des flèches le long desquelles le foncteur tiré-en-arrière n'admet pas d'adjoint à droite. Lorsqu'on se restreint à la catégorie des 1-catégories, une caractérisation “facile” de ce type de flèches a été mise en évidence par J. Giraud en 1964 et indépendamment par F. Conduché en 1972.

Dans cet exposé, je présenterai le travail de Giraud sur la question et j'expliquerai comment l'étendre au cas des infini-catégories strictes. J'expliquerai ensuite pourquoi cette question de non-universalité des colimites est intimement liée à une question de stabilité des résolutions polygraphiques par tiré-en-arrière et cela me permettra d'achever la démonstration d'un résultat laissé en suspens lors de mon exposé du 16/02/2018.

Higher categories, polygraphs and homotopy
Friday February 16, 2018, 2PM, Salle 1007
Léonard Guetta (IRIF) Homologie des 1-catégories

Dans leur article de 2009, “Polygraphic resolutions and homology of monoids”, Y. Lafont et F. Métayer démontrent que l'homologie “polygraphique” des monoïdes coïncide avec l'homologie “habituelle” des monoïdes, c'est-à-dire celle définie avec le foncteur Tor. Je présenterai dans cet exposé une extention du résultat précédent à toutes les 1-catégories. Pour cela, j'établirai un cadre abstrait dans lequel je réinterpréterai les étapes-clés de la démonstration de Lafont-Métayer.

Assez curieusement, cela m'a également amené à étendre certains résultats de Conduché et Giraud sur l'exponentiabilité des 1-foncteurs dont je parlerai également (éventuellement en détails dans un exposé futur).

Mot-clés : Polygraphes, Homologie des 1-catégories, Ext-Tor, Fibrations de Conduché, “push-forward” pour les (n-)catégories.

Higher categories, polygraphs and homotopy
Friday February 2, 2018, 2PM, Salle 1007
Antoine Chambert-Loir (IMJ) Algèbre homologique moderne — comment échapper à « Ignoramus et ignorabimus » ?

Depuis le début du 20e siècle, l'algèbre homologique s'est développée par mues successives, des nombres de Betti aux (∞,1)-catégories en passant notamment par les catégories dérivées. Des développements récents, j'essayerai de discuter le contraste entre complexité (celle que je ressens à la lecture des ouvrages de Lurie, par exemple) et efficacité (je donnerai des exemples tirés de la géométrie algébrique), avec l'œil d'un géomètre qui aimerait bien disposer de ces outils sans pour autant savoir se dépêtrer de la littérature (in-?)existante.

Year 2017

Higher categories, polygraphs and homotopy
Friday November 10, 2017, 2PM, Salle 1007
Mathieu Anel Un argument du petit objet pour les systèmes de factorisation unique

L’argument du petit objet est une recette pour construire des factorisations de morphisme f:X \to Y en f=R(f)L(f) où L(f) et R(f) sont dans des classes L et R qui ont des propriétés de relèvement non-unique (orthogonalité faible) entre elles. Lorsque la propriété de relèvement de L et R est unique (orthogonalité forte) l’argument doit être modifié pour produire la bonne factorisation. Le but de l’exposé sera de proposer deux méthodes pour corriger la construction (inspirées de Gabriel-Ulmer et de Kelly).

Higher categories, polygraphs and homotopy
Friday October 27, 2017, 2PM, Salle 1007
Eric Finster The Generalized Blakers-Massey Theorem

Higher categories, polygraphs and homotopy
Friday September 22, 2017, 2PM, Salle 1007
Simon Henry Les polygraphes non-unitaires et la conjecture de Simpson

Je partirai de deux “théorèmes” faux : Le premier est dû à Kapranov et Voevodsky et dit essentiellement que l'on peut représenter les types d'homotopie par des infini-catégories strictes dont toutes les flèches sont faiblement inversibles. Le deuxième est la preuve par Johnstone et Carboni (et Batanin) que la catégorie des polygraphes est une catégorie de préfaisceaux.

Les deux énoncés sont faux pour des raisons très similaires : à chaque fois l'argument clé est l'argument de Eckmann-Hilton, c'est-à-dire le fait que la composition des endomorphismes de n'importe quelle identité dans une infini-catégorie est strictement commutative. Cette commutativité est incompatible avec les deux affirmations précedentes.

Pour cette raison, il est conjecturé que si l'on travaille dans une situation où il n'y pas d'unité, ou bien où les unités sont faibles ou n'interviennent pas alors ces énoncés deviennent vrais. Dans le premier cas il s'agit de la conjecture de semi-strictification de Simpson qui affirme que les types d'homotopie peuvent être représentés par des infini-catégories strictes “sans identités” qui admettent des identités faibles et des inverses faibles. Dans le deuxième cas il s'agit d'une “conjecture” de Johnstone et Carboni qui dit que la catégorie des polygraphes tels que la source et le but de chaque générateur n'est pas une identité est une catégorie de préfaisceaux.

Dans l'exposé je présenterai une preuve de cette dernière “conjecture” et j'expliquerai en quoi cela pourrait permettre d'arriver à une preuve de la conjecture de Simpson.

Higher categories, polygraphs and homotopy
Friday June 30, 2017, 2PM, Salle 1007
Andrew Polonsky Lambda Calculus is a Groupoid

We discuss the problem of equality in type theory. We present an approach to defining higher equality structures in type theory. As an application, we study the lambda calculus from the multi-dimensional point of view. Taking equality between lambda terms (1-cells) to be beta conversion modulo permutation of redexes, we discover that the induced higher structure is a homotopy 1-type. That is, whenever there exists a higher cell between two β-conversions, the space of such cells is contractible. The key property of the lambda calculus responsible for this is Lévy’s projection calculus (AKA calculus of residuals). We conclude that the result holds for any theory which admits a presentation with such a calculus. For example, all (weakly) orthogonal TRSs describe homotopy 1-types.

Higher categories, polygraphs and homotopy
Friday June 23, 2017, 2PM, Salle 1007
Cyrille Chenavier Borne supérieure des opérateurs de réduction et calcul des syzygies

Higher categories, polygraphs and homotopy
Friday June 16, 2017, 2PM, Salle 1007
Eric Finster A Type Theoretic Definition of Weak Omega-Categories

Higher categories, polygraphs and homotopy
Friday June 2, 2017, 2PM, Salle 1007
Léonard Guetta Quelques remarques sur les modèles acycliques, d'après M.Barr

En 1953, S. Eilenberg et S. Maclane publient l'article “Acyclic Models” dans lequel ils exposent le théorème (ou méthode) dit des modèles acycliques. Cet outil permet de comparer efficacement différentes théories homologiques tout en étant très économe en calculs. Depuis, différents théorèmes dit de «modèles acycliques» ont été démontrés, comme par exemple celui de M.Barr et J. Beck en 1966. Pourtant même si ce dernier a des conclusions similaires au théorème d'Eilenberg et Maclane, le cadre semble assez différent. Dans mon exposé, je présenterai un théorème d'algèbre homologique très général duquel il est très facile de déduire ces différents théorèmes de modèles acycliques ainsi que les théorèmes habituels de relèvement d'algèbre homologique.

Je présenterai aussi mes travaux en cours qui visent à démontrer un théorème de relèvement plus fin et plus général que les précédents et dont un cas particulier a également été démontré par M. Barr dans les années 90. Enfin, si le temps me le permet, j'exposerai un théorème des modèles acycliques d'A. Prouté (non-publié) qui rentre naturellement dans ce nouveau cadre.

Higher categories, polygraphs and homotopy
Friday April 28, 2017, 2PM, Salle 1007
Martin Szyld A general limit lifting theorem for 2-dimensional monad theory

Higher categories, polygraphs and homotopy
Friday April 21, 2017, 2PM, Salle 1007
Eric Hoffbeck Théorie d'obstruction pour les algèbres sur une opérade

Higher categories, polygraphs and homotopy
Friday March 10, 2017, 2PM, Salle 1007
Simon Henry Sur des nouveaux modèles algébriques des types d'homotopie

Dans son manuscrit “À la poursuite des champs” Grothendieck propose une définition “d'infini-groupoïde” ainsi qu'une notion d'équivalence entre eux et conjecture que la catégorie homotopique est équivalente à sa catégorie des infini-groupoïdes “à équivalence près”.

Cette conjecture (l'hypothèse d'homotopie) est toujours un problème ouvert, et il y a de très nombreuses questions basiques concernant cette notion d'infini-groupoïdes qui restent sans réponse. Pour cette raison, on préfère généralement utiliser les ensembles simpliciaux et les complexes de Kan pour définir la notion d'infini-groupoïde et servir de point de départ pour la théorie des catégories supérieures.

Cela dit l'apparition de la théorie homotopique des types nous donne de nouvelles motivations pour s'intéresser à cette notion d'infini-groupoïdes : tout d'abord n'importe quel type en théorie homotopique des types porte une structure d'infini-groupoïde au sens Grothendieck, ensuite, si la théorie des types est censée être la logique interne de certaines infini-catégories, il s'agit à priori d'infini-catégories globulaires, i.e. d'un genre plus proche de la définition de Grothendieck que des versions simpliciales. Enfin, on sait internaliser en théorie des types la définition d'infini-groupoïdes de Grothendieck, alors qu'on est très loin de savoir faire de même pour les approches simpliciales.

Dans cet exposé je vais présenter une nouvelle famille de définitions de la notion d'infini-groupoïde qui sont inspirées de celle de Grothendieck, et qui conservent certaines de ses bonnes propriétés, mais qui échappent aux problèmes de celle-ci et pour laquelle on sait en particulier prouver l'analogue de l'hypothèse d'homotopie.

On énoncera aussi une conjecture technique précise, d'apparence simple, qui impliquerait que la définition de Grothendieck est un cas particulier de la nôtre, et qui donc impliquerait aussi l'hypothèse d'homotopie et résoudrait une partie des problèmes ouverts concernant la définition de Grothendieck.

Higher categories, polygraphs and homotopy
Friday March 3, 2017, 2PM, Salle 1007
Maxime Lucas Structure simpliciale sur les n-branchements et acyclicité de polygraphes

Higher categories, polygraphs and homotopy
Friday February 24, 2017, 2PM, Salle 1007
Cyrille Chenavier Caractérisation et construction de bases de Gröbner par les opérateurs de réduction

Higher categories, polygraphs and homotopy
Friday February 3, 2017, 2PM, Salle 1007
Mathieu Anel Pourquoi les infini-catégories sont-elles utiles ?

En me limitant aux (infini,1)-catégories, j’illustrerai pourquoi on a besoin des catégories supérieures. La réponse que je développerai est que certains axiomes formulables en théorie des catégories n’ont aucun modèles non-triviaux dans les catégories ordinaires mais pas dans les catégories supérieures. L’une de ces propriétés est « l’effectivité des colimites » (forme améliorée de la propriété d’univalence) qui est à la base des infini-topos. Un autre exemple est la propriété de « stabilité » qui simplifie drastiquement la compréhension et la manipulation de l’algèbre homologique.

Higher categories, polygraphs and homotopy
Friday January 27, 2017, 2PM, Salle 1007
Rémy Tuyeras Elimination des quotients dans les modèles d'esquisses limites

Higher categories, polygraphs and homotopy
Friday January 20, 2017, 2PM, Salle 1007
Alexandre Quesney Opérades Swiss Cheese et décompositions cellulaires

Year 2016

Higher categories, polygraphs and homotopy
Friday December 16, 2016, 2PM, Salle 1007
Jacques Penon Une pseudo-adjonction cachée derrière un théorème de M.Weber (II)

Higher categories, polygraphs and homotopy
Friday December 2, 2016, 5:30PM, Salle 3052 * Journées du GDR Topologie Algébrique : changement d'horaire et de salle *
Jacques Penon Une pseudo-adjonction cachée derrière un théorème de M.Weber
Journées du GDR Topologie Algébrique

Higher categories, polygraphs and homotopy
Friday November 4, 2016, 2PM, Salle 1007
François Métayer Algèbres de la monade des états

Higher categories, polygraphs and homotopy
Friday October 28, 2016, 2PM, Salle 1007
Maxime Lucas (IRIF) Inversibilité dans les omega-catégories cubiques

Higher categories, polygraphs and homotopy
Friday October 14, 2016, 2PM, Salle 1007
Simon Forest Une généralisation des complexes de parité de Street et des pasting schemes de Johnson

Higher categories, polygraphs and homotopy
Friday July 8, 2016, 2PM, Salle 1007
Pierre Cagne Bifibrations sur des catégories de modèles et construction de Reedy

Dans cet exposé, je présenterai un théorème permettant de relever une structure de catégorie de modèles le long d'une bifibration dont les fibres ont elles-mêmes un bon comportement homotopique. Ce résultat généralise deux théorèmes de la littérature (le premier par Roig et Stanculescu, le deuxième par Harpaz et Prasma) et a été motivé par l'étude de la construction de Reedy.

Celle-ci est un outil primordial en algèbre homotopique, qui permet de munir d'une structure de catégorie de modèles une catégorie de diagrammes à valeurs dans une catégorie de modèles quand la catégorie index admet de bonnes propriétés. Cette construction passe par l'utilisation de deux foncteurs, le latch et le match, dont l'introduction pourrait paraître a priori ad hoc. Après les rappels nécessaires, je montrerai qu'il n'en est rien et qu'ils sous-tendent en fait une bifibration dont l'étude, via notre théorème, éclaire l'étape clé dans la construction de Reedy.

Si le temps le permet, j'esquisserai rapidement quelques généralisations existantes de la construction de Reedy dans lesquelles la vue bifibrationnelle s'intègre également.

Higher categories, polygraphs and homotopy
Friday July 1, 2016, 2PM, Salle 1007
Albert Burroni Faisceautisation des structures par approximations successives

Classiquement, la construction universelle qui transforme un préfaisceau, de base une catégorie C, en faisceau sur un site (C,T), où T est une topologie de Grothendieck, s'appelle la “faisceautisation”.

En remplaçant le site précédent par une esquisse projective (C,T) où T est un ensemble de cônes projectifs, la notion de structure algébrique, relative à cette esquisse, généralise celle de faisceau. Dans ce cas plus général, une construction similaire, encore appelée faisceautisation, prolonge la construction précédente.

Ces constructions sont basées sur une transformation sur les préfaisceaux qui est itérée de manière transfinie (dont la longueur dépend de la taille des cônes projectifs) et s'inspirent de la technique des “approximations successives” en analyse. Dans le cas des faisceaux la construction s'arrête dès la deuxième étape, nous tenterons d'expliquer pourquoi. On verra aussi comment cette construction s'étend de manière relative aux esquisses mixtes (lesquelles comportent, en plus des cône projectifs de T, des cônes inductifs).

Higher categories, polygraphs and homotopy
Friday June 17, 2016, 2PM, Salle 1007
Eric Hoffbeck Shuffles d'arbres

Higher categories, polygraphs and homotopy
Friday May 20, 2016, 2PM, Salle 1007
François Métayer Monadicité des omega-catégories sur les polygraphes

Higher categories, polygraphs and homotopy
Friday May 13, 2016, 2PM, Salle 1007
Clément Alleaume Décroissance et présentations cohérentes

Higher categories, polygraphs and homotopy
Friday April 15, 2016, 2PM, Salle 1007
Maxime Lucas Une version cubique du théorème de Squier

Higher categories, polygraphs and homotopy
Friday March 25, 2016, 2PM, Salle 1007
Samuel Mimram Parités complexes

Higher categories, polygraphs and homotopy
Friday March 18, 2016, 2PM, Salle 1007
Jacques Penon Algèbre sur une opérade, un éclaircissement

Higher categories, polygraphs and homotopy
Friday March 11, 2016, 2PM, Salle 1007
Brice Halimi Présentation de la théorie des esquisses

Higher categories, polygraphs and homotopy
Friday February 19, 2016, 2PM, Salle 1007
Joey Beauvais-Feisthauer Bicatégories et cohérence

Higher categories, polygraphs and homotopy
Friday February 12, 2016, 2PM, Salle 1007
Albert Burroni Une revisitation (et plus) de la définition des catégories globulaires monoïdales de Batanin

Higher categories, polygraphs and homotopy
Friday January 22, 2016, 2PM, Salle 1007
François Métayer Polygraphes généralisés

Year 2015

Higher categories, polygraphs and homotopy
Friday December 18, 2015, 2PM, Salle 1007
Cyrille Chenavier Opérateurs de réduction II : réécriture et complétion

Higher categories, polygraphs and homotopy
Friday December 11, 2015, 2PM, Salle 1007
Sinan Yalin Espaces de modules de bigèbres, cohomologie de Hochschild supérieure et formalité

Higher categories, polygraphs and homotopy
Friday December 4, 2015, 2PM, Salle 1007
Cyrille Chenavier Opérateurs de réduction I : structure de treillis et confluence

Higher categories, polygraphs and homotopy
Friday November 20, 2015, 2PM, Salle 1007
Jonas Frey Topos de réalisabilité comme catégories d'homotopie

Higher categories, polygraphs and homotopy
Friday November 6, 2015, 2PM, Salle 1007
Pierre-Louis Curien et Jovana Obradovic Polytopes engendrés par des hypergraphes, d'après Dosen et Petric

Higher categories, polygraphs and homotopy
Friday October 23, 2015, 2PM, Salle 1007
Maxime Lucas Polygraphes pour catégories cubiques

Higher categories, polygraphs and homotopy
Friday October 16, 2015, 2PM, Salle 1007
Maxime Lucas Ensembles cubiques symétriques et (omega,n)-catégories cubiques

Higher categories, polygraphs and homotopy
Friday October 2, 2015, 2PM, Salle 1007
François Métayer Nerf de Street et complexe normalisé

Higher categories, polygraphs and homotopy
Friday September 25, 2015, 2PM, Salle 1007
Yves Guiraud Le théorème de Squier pour les algèbres II

Higher categories, polygraphs and homotopy
Friday September 18, 2015, 2PM, Salle 1007
Yves Guiraud Le théorème de Squier pour les algèbres I