Cet exposé est une introduction au catégories extriangulées. La notion de catégorie exacte (au sens de Quillen) est une axiomatisation des sous-catégories de catégories abéliennes, stables par extensions. Le catégories extriangulées sont une tentative d'axiomatisation analogue adaptée au cas des sous-catégories de catégories triangulées, stables par extensions. Après avoir donné des exemples provenant de la combinatoire et de la théorie des représentations, j'expliquerai cette axiomatisation et montrerai comment elle peut être utilisée dans des situations variées. Il s'agit de plusieurs travaux en commun avec Hiroyuki Nakaoka et avec Xin Fang, Misha Gorsky, Osamu Iyama, Arnau Padrol, Vincent Pilaud, Pierre-Guy Plamondon, Matt Pressland.

Descent theory is a set of ideas for reconstructing global structures from local data. The typical example is that we can define a continuous function by recollecting its restrictions on a family of open sets covering the base space. On the other hand, a presheaf is usually defined as the data of a functor from a base category into Set. This approach makes the choice of presentation of the base category somehow “invisible”, and if you happen to be a type theorist, it is sorely lacking in “dependent” flavor. The aim of this presentation is to explain my ongoing work on how descent theory inspires me to give another way of defining presheaves—the so-called “indexed presheaves”.

The first part of the talk will be a brief introduction to descent theory, and its 2-categorical version. The second part, less rigorous, will present my current ideas and plans.

Les diopérades, ou polycatégories, encodent des structures algébriques avec plusieurs entrées et plusieurs sorties, généralisant les opérades. Je montrerai que les foncteurs Frobenius monoïdaux sont exactement ceux qui préservent les algèbres sur une diopérade, généralisant la relation bien connue entre les foncteurs lax monoïdaux et les opérades. Dans un deuxième temps, j'expliquerai comment construire de telles structures Frobenius monoïdales (décalées) en présence d'une donnée d'orientation, de manière analogue à la procédure d'intégration le long des fibres induite par la dualité de Poincaré. La motivation initiale de ce projet vient de la géométrie dérivée, pour laquelle il serait nécessaire d'étendre la construction précédente au contexte ∞-catégorique. Je terminerai en exposant les difficultés homotopiques posées par cette généralisation. Il s'agit d'un travail en collaboration avec Valerio Melani.

La théorie des catégories test de Grothendieck permet de caractériser les petites catégories dont la catégorie des préfaisceaux modélise (après une localisation appropriée) les types d'homotopie. Toute catégorie test est alors “aussi bonne” que la catégorie des simplexes pour faire de la théorie de l'homotopie.

Mais la catégorie des simplexes possède d'autres propriétés utiles en topologie algébrique. Parmi elles figure la “correspondance de Dold-Kan homotopique” : les groupes abéliens simpliciaux forment aussi un modèle des types d'homologie, après une localisation appropriée.

Dans cet exposé, je décrirai un cadre permettant de chercher des correspondances de Dold-Kan homotopiques pour les préfaisceaux en groupes abéliens sur des petites catégories quelconques, et en particulier sur les catégories test. Je donnerai également une classe d'exemples incluant, entre autres, la catégorie Thêta de Joyal.

Depuis la célèbre hypothèse d'homotopie formulée par Grothendieck, un thème central de la théorie de l'homotopie et de l'algèbre supérieure consiste à décrire les théories homotopiques d'objets géométriques et topologiques à l'aide de modèles algébriques. Parmi les correspondances fondamentales entre géométrie/topologie d'un côté et algèbre de l'autre, on peut citer :

  Types d'homotopie ↔ oo-groupoïdes
  Spectres ↔ oo-groupoïdes symétriques monoïdaux
  Catégories topologiques ↔ (oo,1)-catégories
  n-cobordismes ↔ Objets dans une (oo,n)-catégorie monoïdale avec duaux libres sur un objet
  n-champs localement constants sur un espace X ↔ Représentations du (pro)-n-groupoïde fondamental de X

Mais qu'entend-on exactement par “modèle algébrique” ? Suivant le point de vue adopté pour répondre à cette question, le statut des correspondances énoncées oscille entre conjectures et théorèmes.

Dans cet exposé, je proposerai un cadre général – la théorie des canevas – qui permet de formaliser précisément cette notion de “modèle algébrique” et de revisiter certaines de ces correspondances sous un angle unifié. Ce cadre nous offrira l'occasion d'aborder des thématiques variées, telles que la théorie des catégories tests, la transition des opérades simpliciales vers les oo-opérades, ou encore les divers résultats de rigidification des structures supérieures.

Si le temps le permet, je présenterai également un vaste programme de conjectures et de questions naturelles émanant de ce cadre, ainsi que certains de mes travaux qui s'inscrivent dans cette perspective.

La cohomologie d'un espace est classiquement définie à partir de son complexe de cochaînes singulier. Ce-dernier n'étant pas lui-même un invariant homotopique, on ne peut pas espérer une définition similaire de la cohomologie en HoTT. À la place, on passe par la représentabilité de la cohomologie par les espaces d'Eilenberg-Maclane K(G,n). Le but de cet exposé est de montrer comment traduire mot à mot le langage des torseurs et des gerbes de la théorie des faisceaux vers la théorie des types pour aboutir à la construction de types K(G,1) et K(G,2).

A framed polytope is the convex closure of a finite set of points in Euclidean space together with an ordered linear basis. An n-category is a category that is enriched in the category of (n-1)-categories. Although these concepts may initially appear to be distant peaks in the mathematical landscape, there exists a trail connecting them, blazed in the 90's by Kapranov and Voevodsky. We will traverse this path, widening and improving it as we address some of their conjectures along the way. If time permits, using a special embedding of the combinatorial simplex, we will connect this trail to the one ascending Mount Steenrod. This connection will enable us to express the combinatorics of cup-i products in convex geometric terms, dual to those introduced earlier in the talk to define the nerve of higher categories.

Dans cet exposé, je vais présenter des travaux concernant le calcul de témoins de naturalité des opérations dans les omega-catégories faibles. Intuitivement, les témoins de naturalité traduisent du fait que chacune des opération d'une omega-catégorie faible se doit d'être un omega-foncteur faible. Bien que l'on manque d'outils pour exprimer formellement cette intuition, on peut explorer ce que cela signifie en petite dimension, ce qui amène à une notion que l'on a appelée la fonctorialité des opération, puis dans un second temps à la notion de naturalité. Je vais esquisser une construction permettant d'obtenir un témoin de naturalité associé à chacune des opérations d'une omega-catégorie, en m'appuyant sur la combinatoire des carrés et de leur composition. J'illustrerai ensuite cette construction en introduisant les cellules d'Eckmann-Hilton, et en montrant que la construction des témoins de naturalité permet de déduire des cellules d'Eckmann-Hilton en dimension supérieures à partir de celles en petites dimension.

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.

In my talk, I will discuss the category $pOpe_\iota$ of positive opetopes with \iota-contractions, introduced by Zawadowski. I will then define the category $\widehat{pOpe_\iota}_{EZ}$ of Eilenberg-Zilber opetopic sets, which are presheaves on $pOpe_\iota$ analogous to simplicial sets. I will outline a modification of Cisinski theory applicable to $\widehat{pOpe_\iota}_{EZ}$, demonstrating the existence of a model structure. Additionally, I will sketch the proof of its Quillen equivalence to the Kan-Quillen model structure. If time allows, I will touch upon another model structure and its potential comparison with the Joyal model structure on simplicial sets.

Model categories provide a good environment to do homotopy theory. A model category consists of a bicomplete category together with three classes of morphisms (weak equivalences, cofibrations, and fibrations) satisfying a list of axioms. While weak equivalences are the main players in a model category and encode how two objects should be thought of as being ``the same, the additional data of cofibrations and fibrations typically facilitates computations of homotopy limits and colimits, and of derived functors. However, because of their robust structure, model categories are usually hard to construct. In joint work with Guetta, Sarazola, and Verdugo, we develop new techniques for constructing model structures from given classes of cofibrations, fibrant objects, and weak equivalences between them. The requirement that one only needs to provide a class of weak equivalences between fibrant objects both simplifies the conditions to check and seems more natural in practice: often, the fibrant objects are the ``well-behaved objects in a model category and so the weak equivalences should only be expected to exhibit a good behavior between these objects. As a straightforward consequence of our result, we obtain a more general version of the usual right-induction theorem along an adjunction, where fibrations and weak equivalences are now only right-induced between fibrant objects; we refer to such an induced model structure as fibrantly-induced.

As applications of these new methods, we construct several model structures on the category of double categories.

La construction de Grothendieck est une construction fondamentale de la théorie des catégories. Dans cet exposé, j'en donnerai une généralisation dans le cadre des $\omega$-catégories faibles. À cette fin, je présenterai quelques concepts importants de la théorie des $\omega$-catégories faibles, tels que les transformations lax, les (co)limites lax, et les fibrations cartésiennes. Enfin, j'expliquerai comment ce résultat peut être utilisé pour donner des calculs explicites d'extensions de Kan lax.

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

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.

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.

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.

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.

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.

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.

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

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 (https://hal.science/hal-03702762), as well as a long version of that article in preparation.

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.

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 : https://u-paris.zoom.us/meeting/register/tZUtdOmuqj4pGNz_ymC1VNXs6xhvCfd7Sprs

Concurrent Kleene algebra, introduced by Tony Hoare et.al. 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). https://arxiv.org/abs/2106.10895 - Catoids and Modal Convolution Algebras. Algebra Universalis 84(10) (2023). https://link.springer.com/article/10.1007/s00012-023-00805-9

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.

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.

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.

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.

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.

https://arxiv.org/abs/2209.08022

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.

https://arxiv.org/abs/2202.09293 ; https://arxiv.org/abs/2210.07704

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

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.

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

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.

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.

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.

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.

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 : https://arxiv.org/abs/2203.07046

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.

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.
4. …

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.

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.

Référence: https://arxiv.org/abs/2110.14062

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.

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

http://www.numdam.org/item/CTGDC_1981__22_3_249_0.pdf

Travail mené conjointement avec Eric Finster et Matthieu Sozeau (https://arxiv.org/abs/2105.00024).

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.

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

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

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

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 : arxiv.org/abs/2102.04281

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

https://www.irif.fr/~metayer/GDT/resume_18_10_19.pdf

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.

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.

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.

References

1. Axiomatic homotopy theory for operads (arxiv.org/abs/math/0206094)

2. The Boardman-Vogt resolution of operads in monoidal model categories (arxiv.org/abs/math/0502155)

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.

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

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.

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 https://maths.tcd.ie/~pedro/MON19.pdf

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

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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