Categorical Applications and Foundations Exchange

Orthocoproduct Semantics of Reversible Programming
— Louis Lemonnier (University of Edinburgh)

This talk brings a categorical look at reversible programming with 'orthocoproducts'. The latter are coproducts, but restricted by a notion of orthogonality, with a connection to Simpson's independence pullbacks. For syntax, we use the symmetric pattern matching language introduced by Sabry, Valiron, and Vizzotto as a reference point, and we incorporate several improvements in the type system.

Categories with indexed monoids
— Leo Lobski (University College London)

It is well-known that equipping each object in a symmetric monoidal category with a comonoid in a way that is natural and uniform with respect to the monoidal structure is equivalent to the monoidal category being cartesian monoidal (this is Fox's theorem). In this talk, we further equip each object with a monoid, and ask this choice of monoids to be uniform but not necessarily natural. Such a cartesian monoidal category with chosen monoids is called a category with indexed monoids. After covering some examples, we show how to construct the free category with indexed monoids on any (small) category. We then extend the notion of indexed monoids to opfibrations, and show that opfibrations with indexed monoids are equivalent to the choice of a monoid on the category of opfibrations with a fixed base. We conclude by relating this to (op)indexed monoidal categories via a result of Moeller & Vasilakopoulou. The talk is based on Section 4 of "Layered Monoidal Theories II: Fibrational Semantics", which, in turn, is based on Chapter 7 of my PhD thesis.

Pasting theorems: sufficient conditions for strictification
— Clémence Chanavat (Tallinn University of Technology)

It is well known that a tricategory is, in general, not equivalent to a strict 3-category. Similarly, few (∞,1)-categories are equivalent to 1-categories. A natural question arises: when is a given homotopy-coherent higher structure equivalent to a strict one? In this talk, we will formally set up this problem and, based on our latest work [Cha26], give the most general answer currently available in the literature for (∞,n)-categories. If time allows, we will discuss the case of n-tuple categories, and how our methods could be used to expand the existing pasting theorems available for these structures.

[Cha26] C. Chanavat. A strengthened (∞, n)-categorical pasting theorem, 2026.

Interleaving Actions and Effects, Monoidally
— Niels Voorneveld (Cybernetica)

We start with a categorical description of interleaving concurrency for actions in a join-semilattice enriched category. This uses "fork" and "merge" operation, which allow for intuitive representation in string diagrams; that is strings are seen as computational threads which can be split and distributed, as well as brought together. We then generalize to interleaving concurrency for (algebraic) effects, and interleaving processes with semantics given by potentially non-commutative monads. This talk will cover both past and unpublished work.

Monoidal Substitution Diagrams
— Samuel Steakley (Tallinn University of Technology)

The goal of this project is to give a construction of free symmetric monoidal closed (SMClosed) categories in the form of a category where objects are monoidal dependency graphs, and morphisms are monoidal substitution diagrams. Both monoidal dependency graphs, and monoidal substitution diagrams, are certain classes of directed acyclic graphs, equipped with a little extra structure. Previous graphical constructions of free SMClosed categories have not taken advantage of the strictifiability of the currying and unit isomorphisms of monoidal closed structure. Examination of our graphical language suggests that the strictness of the monoidal closed isomorphisms is a decisive factor that helps give the diagrams a unique degree of visual intuition. This talk will introduce both monoidal dependency graphs and monoidal substitution diagrams, and time permitting, give a snapshot of the current status of this work-in-progress.

This is joint work with Florian Schwarz (University of Calgary).

Complete positivity with respect to the direct sum?
— Cole Comfort (Inria)

Selinger's CPM construction takes a compact closed category, and produces a dagger-compact closed category of abstract quantum channels in that category. Notably, when applied to the dagger compact closed category of finite dimensional Hilbert spaces with respect to the tensor product, this produces the category of completely positive maps between finite-dimensional matrix algebras. We show that the CPM construction can be generalised dagger categories with respect to the biproduct. We show that when applied to the dagger symmetric monoidal category of Hilbert spaces with respect to the direct sum, this produces the Markov category of proper Gaussian linear transformations between finite dimensional vector space. Therefore, we find that applying this construction with respect to the tensor adds classical noise to quantum processes, whereas with respect to the direct sum it adds Gaussian probabilistic noise.

What is a contravariant monad?
— Fosco Loregian (Tallinn University of Technology)

Let C be any category. A contramonad on C is a contravariant endofunctor T : Cᵒᵖ → C equipped with suitable dinatural analogues of the unit and multiplication of a monad, satisfying the corresponding axioms. An involutive monad on C is a monad T : C → C whose Kleisli category Kl(T) is equipped with a contravariant self-equivalence J : Kl(T)ᵒᵖ → Kl(T). Examples of involutive monads include presheaf constructions and, in particular, the powerset monad. The latter also gives rise to a contramonad via the contravariant powerset functor, which can then be endowed with a monad structure without resorting to the trick of passing to its adjoint.

Few people suspect the existence of contramonads; even fewer are aware that contramonads and involutive monads are in fact equivalent notions. This was established by René Guitart in his 1975 paper Monades involutives complémentées (1975), which itself is the culmination of a sequence of extremely terse Comptes Rendus notes published during the first half of the 1970s. "Terse" should be interpreted literally: Comptes Rendus contain no proofs, whereas the long Cahiers paper contains only four commutative diagrams across 86 pages of equational reasoning. Perhaps because of the style of these papers, the notion of contramonad never gained much traction. In this talk I will revisit Guitart's equivalence, explain why it is conceptually compelling, and argue that it deserves renewed attention. I will also suggest that the notion of contramonad is sufficiently formal to admit a formulation in 2-categories more general than Cat. No new results will be presented, although the approach is in part new: Guitart's proof is in the process of being fully formalized in agda-categories.