Operads Formalization

Stream: mathlib4

[Adrian Marti]

Hi all, hope you have a great new year :)

I finished a fully dependently typed formalization of (coloured) operads over on my mathlib fork. It is based on the notion of a profunctor, i.e. for me a coloured operad on a category $C$ (in most cases, this is just a discrete set of objects) is a certain profunctor equipped with a composition and a unit that satisfy associativity and unit laws. In my setup, these turned out to be not too bad to write down, despite the dependent type.

My formalization is based on the abstraction of what in my file is referred to as a monad of profunctors. This is meant to encapsulate a notion of a monad on a virtual equipment, meaning that we send profunctors to profunctors and functors to functors in a compatible way and moreover, we send units (natural transformations with zero inputs), natural transformations and binatural transformations (natural transformations with two inputs) to their counterparts on the target. MonadProf does omit some of the required axioms, since I did not need them, making the definition a bit ad-hoc (subject to change in the future).

In any case, this MonadProf abstraction lets us insert different monads to get the different flavours of operads: planar, symmetric and cartesian (or even semicartesian), which is a super useful feature. I have not yet written up the constructions for these monads and the corresponding instances for MonadProf.

So far, I've played with a number of different definitions of operads, and I would say that I like this current one the most.

I was wondering whether the mathlib community has any thoughts on merging this into mathlib soon. Should I PR it? There are a couple of obvious things that are not there yet.

• Constructions of the different monads giving rise to different flavours of operads
• Defining more generally usable abstractions for FunctorProf so that we can send a general natural transformation with n inputs to a natural transformation with n inputs on the target and stating the missing axioms.
• Maybe some examples as test cases?

I am sure there are also a number of minor things, like documentation or splitting up into more files that should be done before merging. Also, I would be happy to provide an explanation of how this FunctorProf and MonadProf thing works if someone would like me to expand on it :)

[Adrian Marti]

P.S. There are some simple diagrams (in a virtual equipment, i.e. involving functors, profunctors and 2-cells with n inputs) that give rise to the operad laws as I formalized them. They greatly helped me understand what is going on, so I made a quick sketch.
2026-01-02-Operad diagrams.pdf

[Dagur Asgeirsson]

@Adam Topaz and I have been working on a different implementation of profunctors. We should coordinate and make sure we find a good approach (although I have family obligations for the next few weeks and it’s unclear how much time I’ll have for Lean).

[Robin Carlier]

First off, congratulations for finding a framework that minimizes the amount of DTT Hell for this!

So that we don't end up all stepping on each other toes, I'll mention that I am also working on something a bit related: interpretations of symmetric monoidal categories in "unbiased" frameworks (specifically infty-operads à la Lurie, but without defining them directly for now: I'm content with just producing a fibration over/pseudofunctor out of finite pointed sets that has the expected properties.). Hopefully, some of the output of what I'm doing could help you give a constructor for a symmetric operads out of a symmetric monoidal category.

Cruttwell and Shulman mention this as 9.6 in their paper: these operads/multicategories based approaches produce "unbiased" things, and there is a nontrivial amount of work to do to to go from the biased constructors (where you give only "low-arity" operations and coherences) to the unbiased ones that can be used in frameworks like the one you are defining here: in the case of symmetric monoidal categories, Maclane's coherence theorem (the symmetric version) has to be used.

[Adrian Marti]

@Dagur Asgeirsson I would love to get profunctors into mathlib and coordiinate! There are two obvious approaches that I can think of, either take functors Cᵒᵖ × C ⥤ Type u or functors `Cᵒᵖ ⥤ C ⥤ Type u (curried). There is also the question of whether to op on the left or on the right. Honestly, most of these issues don't matter too much to me, as long as a basic API is there.

Of course, getting a bicategory instance through profunctor composition would be nice. In this case, however, I have explicitly avoided profunctor composition by allowing 2-cells with multiple input profunctors (in part, because I have an application where computability is important in mind). So getting an API for working with these more general n-cells would be something I care about, though it's possibly a somewhat niche usecase.

[Robin Carlier]

For profunctors, mathlib would likely prefer the curried version: this tends to work better with automation.

[Adrian Marti]

@Robin Carlier You're right, your n-ary tensor product implementation you posted about before might be useful to do that! And thank you for the interesting remark in the paper, I haven't really read a lot of it! If I need it, I could try making my formalization depend on yours.

It would also be an interesting project to define the "category of operators" together with the functor satisfying the Segal condition to also get the fully unbiased construction of operads (a la Lurie). It might be desirable to have both ideas in mathlib eventually! One perhaps more suitable for concrete constructions and the other for more abstract ideas and comparison with the $\infty$-setting.

[Adrian Marti]

Robin Carlier said:

For profunctors, mathlib would likely prefer the curried version: this tends to work better with automation.

I think that is an easy change for me to make :) I found that I need a constructor to apply profunctors to objects anyways (Prof.app), because the left object lives in the opposite category.

[Adrian Marti]

I have moved the profunctor code to a new file. Do you think the curried version is better, even if the way always goes through the API like Prof.app for application? I'm not an automation expert.

[Robin Carlier]

A general comment: I see you are using (X Y : Cat), usually, in mathlib we tend to write things in an unbundled way, i.e the idiomatic way to write things would be with parameters (X : Type*) [Category* X] (Y : Type*) [Category* Y]. One of the reasons behind this design choice is that it allows for more universe polymorphism (X Y : Cat implicitly means X and Y must have same universe levels for objects and morphisms)

[Adam Topaz]

It's great to hear that others are also interested in getting profunctors into Mathlib! As Dagur mentioned, we have been working on this and settled on the following approach:

universe w

structure Profunctor (C : Type*) [Category* C] (D : Type*) [Category* D] where
  obj : D → C → Type w
  map {X X' : D} {Y Y' : C} (f : X ⟶ X') (g : Y ⟶ Y') :
    obj X' Y → obj X Y'
  map_id (X : D) (Y : C) (e : obj X Y) : map (𝟙 _) (𝟙 _) e = e
  map_comp {X X' X'' : D} {Y Y' Y'' : C}
    (f : X ⟶ X') (f' : X' ⟶ X'')
    (g : Y ⟶ Y') (g' : Y' ⟶ Y'')
    (e : obj X'' Y) :
    map (f ≫ f') (g ≫ g') e = map f g' (map f' g e)

Since the role of Type w here is in the usual type-theoretic sense (not as a category) we ended up getting somewhat bogged down with category theory automation failing due to getting confused between functions and morphisms in Type w (surely anyone who has done category theory in Mathlib has experienced such annoyances). So the first task we wanted to tackle is to introduce a new TypeCat category whose morphisms are one field structures bundling a function, and systematically refactoring the uses of Type w in the category theory library to use TypeCat instead.

[Robin Carlier]

If the refactor bringing in TypeCat goes through, would there still be a need for an ad hoc structure like this for profunctors? I feel like this is just duplicating code for things we already have.
(Edit: oh I guess the point is to not use TypeCat even here. Still not sure about the pros and cons: wouldn't that block using the API for coends that we already have when dealing with compositions of profunctors?)

[Robin Carlier]

(I also agree that a stronger separation between category-theory morphisms and bare functions would be a good thing to help unconfusing automation, but it's probably going to be quite a big refactor. Have there been prior discussions about this or are you taking this thread as an opportunity to announce this upcoming refactor?)

[Adrian Marti]

Robin Carlier said:

A general comment: I see you are using (X Y : Cat), usually, in mathlib we tend to write things in an unbundled way

I'm kind of aware of that and that the way I'm doing profunctors should do it that way. I think I'll leave it to Adam and Dagur to work that part out and use a temporary definition for now. Unless, of course, there is a branch somewhere I can use.

However, the way I'm doing operads using a monad T : Monad Cat, makes it really convenient to have structure Operad (X : Cat) where ..., since I'm constantly calling T.obj X or also T.obj (T.obj X), where I would otherwise have to insert Cat.of everywhere anyways. I hope this is fine.

[Adrian Marti]

Robin Carlier said:

A general comment: I see you are using (X Y : Cat), usually, in mathlib we tend to write things in an unbundled way

I'm kind of aware of that and that the way I'm doing profunctors should do it that way. I think I'll leave it to Adam and Dagur to work that part out and use a temporary definition for now. Unless, of course, there is a branch somewhere I can use.

However, the way I'm doing operads using a monad T : Monad Cat, makes it really convenient to have structure Operad (X : Cat) where ..., since I'm constantly calling T.obj X or also T.obj (T.obj X), where I would otherwise have to insert Cat.of everywhere anyways. I hope this is fine.

In any case, I'm happy to hear that you have been experimenting with profunctors and settled for an approach! I guess I didn't really pay too much attention to the details of this, being focused on the operads part.