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