Rencontre, 5 février 2026

Programme

10:30 – 11:45

Morgan Rogers (LIPN, Université Sorbonne Paris Nord)

Invited talk: What is a monoid?

In many situations one encounters an entity that resembles a monoid. It consists of a carrier and two operations that resemble a unit and a multiplication, subject to three equations that resemble associativity and left and right unital laws. The question then arises whether this entity is, in fact, a monoid in a suitable sense.

Category theorists have answered this question by providing a notion of monoid in a monoidal category, or more generally in a multicategory. While these encompass many examples, there remain cases which do not fit into these frameworks, such as the notion of relative monad and the modelling of call-by-push-value sequencing. In each of these examples, the leftmost and/or the rightmost factor of a multiplication or associativity law seems to be distinguished.

To include such examples, we generalize the multicategorical framework in two stages.

Firstly, we move to the framework of a left-skew multicategory (due to Bourke and Lack), which generalizes both multicategory and left-skew monoidal category. The notion of monoid in this framework encompasses examples where only the leftmost factor is distinguished, such as the notion of relative monad.

Secondly, we consider monoids in the novel framework of a bi-skew multicategory. This encompasses examples where both the leftmost and the rightmost factor are distinguished, such as the notion of a category on a span, and the modelling of call-by-push-value sequencing.

In the bi-skew framework (which is the most general), we give a coherence result saying that a monoid corresponds to an unbiased monoid, i.e. a map from the terminal bi-skew multicategory.

This is joint work with Paul Blain Levy

13:45 – 14:45

Jui-Hsuan Wu (Ray) (LIP, ENS de Lyon)

Invited talk: Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints

Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This alternative presentation provides better structural properties for the analysis of this relation and leads to a simple decision algorithm.

In this talk, I will show how this transitivity-free approach can be extended beyond BCD to a broad class of intersection type systems. The extensions we consider allow imposing some pre-order as well as fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with eta-equality (Scott, Park, etc).

I will then establish the equivalence between these transitivity-free systems and their traditional BCD-style presentations using cut-elimination techniques from proof theory. The presence of fixpoints requires moving beyond standard finite derivations, leading to the use of non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.

This is joint work with Olivier Laurent.

15:15 – 16:15

Raphaëlle Crubillé (LIS, Université Aix-Marseille)

Invited talk: Interpreting De Finetti's Theorem in the Category of Integrable Cones

We establish a connection between two results in the literature on probabilistic semantics: a formulation of De Finetti's theorem in the language of category theory due to Jacobs and Staton, and the generic construction of the free exponential of Linear Logic by Melliès et al, that has been instantiated in the model of probabilistic coherence spaces by Crubillé et al. The structural proximity of these two constructions is manifest, but making this connection formal requires technical developements on the relationship between the category of stochastic kernels and the category of integrable cones, two well-known categories in probabilistic semantics.  We then use this connection to give a characterisation of the total elements of the probabilistic coherence space !Bool.