Looking for feedback: Coloured operads formalization

Stream: maths

[Adrian Marti]

Hi all,
I've been looking for a way to formalize coloured operads (aka multicategories) in Lean over the past few weeks and I've come up with a prototype. In the end I went for a version that bundles arrows together with their source and target, in the following way: A multicategory is a set of arrows A and a set of objects M together with a source map $A \to T M$ and a target map $A \to M$, where T M denotes the type of finite lists Fin n -> M for some n.

Composition then takes a T A and an A together with a proof that the targets and sources match and produces a new arrow A. While it might seem awkward to take a proof as an argument to composition, I found that formalizing multicategories with a dependent type T M -> M -> Type u of multiarrows made it hard to compose and required constantly having to transport along the source and target to compose anything and associativity was tough to state.

So for now I'm using this bundled version for arrows. Here is the formalization. There it also includes multifunctors and at the end a construction for the multicategory associated to a monoidal category (with sorries).

I'd be happy to get any feedback or suggestions for improvement or discuss possible generalizations to the symmetric operad case or even to operads over other categories like vector spaces, simplicial sets or chain complexes. If the design turns out to be good, maybe there might be interest of getting something like this into mathlib.

import Mathlib

namespace CategoryTheory

open CategoryTheory MonoidalCategory

universe u v

/-- Think of this as the objects of a category `Assoc α` encoding
associative lists of elements of `α`. -/
structure Assoc (α : Type _) where
  n : ℕ
  f : Fin n → α

instance instAssocFunctor : _root_.Functor Assoc where
  map f a := ⟨a.n, f ∘ a.f⟩

def single {α} (x : α) : Assoc α := ⟨1,![x]⟩

@[simp]
lemma single_nat {α β} (x : α) (f : α → β) : f <$> single x = single (f x) := by
  sorry

def flatten {α} (a: Assoc (Assoc α)) : Assoc α := {
  n := ∑ i: Fin a.n, (a.f i).n
  f i := Sigma.uncurry (fun i j ↦ (a.f i).f j) (finSigmaFinEquiv.symm i)
}

@[simp]
lemma flatten_nat {α β} (x : Assoc (Assoc α)) (f : α → β) :
    f <$> flatten x = flatten (_root_.Functor.map (f:= _root_.Functor.Comp Assoc Assoc) f x) := by
  sorry

instance instAssocMonad: _root_.Monad Assoc where
  pure := single
  bind x f := flatten (f <$> x)

lemma flatten_single {α} (a : Assoc α) : flatten (single <$> a) = a := by
  sorry

lemma flatten_single' {α} (a : Assoc α) : flatten (single a) = a := by
  sorry

-- The above is really saying that `Assoc` is a monad.
instance instAssocLawfulMonad : LawfulMonad Assoc :=
  sorry

def Assoc.prod {X : Type*} [One X] [Mul X] (x : Assoc X) : X :=
  (List.ofFn x.2).prod

def Assoc.catProd {X : Type*} [Category X] [MonoidalCategory X] : Assoc X → X :=
  @Assoc.prod X (One.mk (𝟙_ X)) (Mul.mk MonoidalCategoryStruct.tensorObj)

def Assoc.single_catProd {X : Type*} [Category X] [MonoidalCategory X] (x : X) :
    catProd (single x) ≅ x := by
  sorry

/-- A span between two types A and B is a space Arr of arrows
together with two morphisms Arr → A and Arr → B. -/
structure Span (A B : Type*) where
  Arr : Type*
  src : Arr → A
  tgt : Arr → B

-- To get the right permutation actions on this, you need the source morphism to be a
-- (discrete) fibration. This then induces the maps `Mul s t → Mul s' t` on the fibers.
-- In this way you can construct symmetric operads

-- Enrichment of multicategories can be done by considering internal vector spaces,
-- chain complexes or simplicial sets internal to `Multiquiver`
-- equipped with the monoidal product of multiquivers.

/-- A multiquiver is a type of arrows, each a source list of objects and a target object. -/
abbrev Multiquiver (obj : Type*) := Span (Assoc obj) obj

/-- The identity multiquiver that with only identity multi-edges. -/
def Multiquiver.Id (obj : Type*) : Multiquiver obj := {
  Arr := obj
  src := single
  tgt := id
}


structure Multiquiver.Mul {obj : Type*} (q : Multiquiver obj) (S : Assoc obj) (T : obj) where
  arr : q.Arr
  src_f : q.src arr = S
  tgt_f : q.tgt arr = T

def uncurryPb {A B C Z: Type*} {f: A → B} {g: C → B}
    (h: (a: A) → (c: C) → (p: f a = g c) → Z): Function.Pullback f g → Z :=
  fun t ↦ h t.fst t.snd t.2

def curryPb {A B C Z: Type*} {f: A → B} {g: C → B}
    (h: Function.Pullback f g → Z): (a: A) → (c: C) → (p: f a = g c) → Z :=
  fun a b p ↦ h ⟨(a,b),p⟩

def Assoc.pullback {A B C: Type u} {f: A → B} {g: C → B}:
    Assoc (Function.Pullback f g)
      ≃ Function.Pullback (_root_.Functor.map (f:=Assoc) f) (_root_.Functor.map (f:=Assoc) g) := by
  sorry

-- This should be refactored to use `CategoryTheory.Functor` instead of the built-in
-- notion of Functor

/-- Lift a function with domain an uncurried pullback through a pullback-preserving functor. -/
def liftPb {A B C Z: Type u} {f: A → B} {g: C → B}
    (h: (a: A) → (c: C) → (p: f a = g c) → Z):
    (a: Assoc A) → (c: Assoc C) → (p: f <$> a = g <$> c) → Assoc Z :=
  curryPb ((_root_.Functor.map (uncurryPb h)) ∘ Assoc.pullback.symm)

@[simp]
lemma liftPb_fst {A B C: Type u} {f: A → B} {g: C → B}
    (x: Assoc A) (y: Assoc C) (p: f <$> x = g <$> y):
      liftPb (fun x _ _ ↦ x) x y p = x := by
  sorry

@[simp]
lemma liftPb_snd {A B C: Type u} {f: A → B} {g: C → B}
    (x: Assoc A) (y: Assoc C) (p: f <$> x = g <$> y):
      liftPb (fun _ y _ ↦ y) x y p = y := by
  sorry

lemma liftPb_map {A B C Z W: Type u} {f: A → B} {g: C → B}
    (h: (a: A) → (c: C) → (p: f a = g c) → Z) (k: Z → W):
    ∀x y p, k <$> liftPb h x y p = liftPb (fun x y p ↦ k (h x y p)) x y p := by
  sorry

class Multicategory (obj: Type*) extends Multiquiver obj where
  /-- Identity arrows. -/
  id: obj → Arr
  src_id: ∀x, src (id x) = single x
  tgt_id: ∀x, tgt (id x) = x
  /-- Arrow composition. -/
  comp: (f: Assoc Arr) → (g: Arr) → tgt <$> f = src g → Arr
  src_comp: ∀f g p, src (comp f g p) = flatten (src <$> f)
  tgt_comp: ∀f g p, tgt (comp f g p) = tgt g
  /-- Right composition with the identity does nothing. -/
  comp_id: ∀x f (p: src f = x), comp (id <$> x) f (by simp [tgt_id, p]) = f
  /-- Left composition with the identity does nothing. -/
  id_comp: ∀f x (p: tgt f = x), comp (single f) (id x) (by simp [p, src_id]) = f
  -- We need to lift the domain of `comp` through `Assoc` to state associativity.
  /-- Associativity of composition. -/
  comp_assoc (f: Assoc (Assoc Arr)) (g: Assoc Arr) (h: Arr)
      (f_comp_g: tgt <$> (_root_.Functor.Comp.mk f) = src <$> g)
      (g_comp_h: tgt <$> g = src h):
    comp (flatten f) (comp g h g_comp_h) (by simp [src_comp, <- f_comp_g]; rfl)
      = comp (liftPb comp f g (by rw [<- f_comp_g]; rfl)) h
        (by simp_rw [liftPb_map, tgt_comp, <- liftPb_map, liftPb_snd, g_comp_h]
      )


open Multicategory

attribute [simp] src_id tgt_id src_comp tgt_comp Multicategory.comp_id Multicategory.id_comp

structure Multifunctor (M N : Type u) [m : Multicategory M] [n : Multicategory N] where
  obj : M → N
  map : m.Arr → n.Arr
  obj_src : ∀f, obj <$> m.src f = n.src (map f)
  obj_tgt : ∀f, obj (m.tgt f) = n.tgt (map f)
  map_id : ∀x, map (m.id x) = n.id (obj x)
  comp_map (f : Assoc m.Arr) (g : m.Arr) (p: _) : comp (map <$> f) (map g)
      (by grind [Functor.map_map])
    = map (comp f g p)

-- TODO: Bicategory instance for multicategory

@[ext]
structure MonoidalCategory.Multiarrow (C : Type u)
    [Category.{v, u} C] [MonoidalCategory C] where
  src : Assoc C
  tgt : C
  arr : src.catProd ⟶ tgt

@[simps]
def MonoidalCategory.MultiarrowOne (C : Type*)
    [Category C] [MonoidalCategory C] (x : C) : Multiarrow C := {
  src := single x
  tgt := x
  arr := (Assoc.single_catProd x).hom ≫ 𝟙 x
}

def MonoidalCategory.MultiarrowProdArr {C : Type*}
    [Category C] [MonoidalCategory C] (f : Assoc (Multiarrow C)) :
    Assoc.catProd (flatten ((·.src) <$> f)) ⟶ Assoc.catProd ((·.tgt) <$> f) := by
  sorry

def MonoidalCategory.MultiarrowProd {C : Type*}
    [Category C] [MonoidalCategory C] (f : Assoc (Multiarrow C)) : Multiarrow C :=
  sorry

open MonoidalCategory

namespace Multicategory

def ofMonoidal (C : Type u) [Category.{u, u} C] [MonoidalCategory C] : Multicategory C := {
  Arr := Multiarrow.{u,u} C
  src x := x.src
  tgt x := x.tgt
  id x := MultiarrowOne C x
  src_id x := rfl
  tgt_id x := rfl
  comp f g p := ⟨flatten ((·.src) <$> f), g.tgt, by
      -- For some reason tactic-mode gives a very significant elaboration speedup.
      exact (MultiarrowProdArr f) ≫ eqToHom (congrArg Assoc.catProd p) ≫ g.arr
    ⟩
  src_comp := by simp only [implies_true]
  tgt_comp := by simp only [implies_true]
  comp_id x f p := by
    sorry
  id_comp := by
    sorry
  comp_assoc := by
    sorry
}


end Multicategory
end CategoryTheory

[Robin Carlier]

I have been thinking about these kind of things as well, but with a different perspective, which is still close to the one you describe: in higher category theory "à la Lurie", the data of a "multicategory" is encoded in the data of a (planar) $\infty$-operad. A planar $\infty$-operad is a functor F : C ⥤ SimplexCategoryᵒᵖ such that so-called "inert" morphisms (of which the opposites of the inclusions ⦋1⦌ ⟶ ⦋n⦌ picking the inequality i ≤ i + 1 are example) have F-cocartesian lifts, and such that, via the lifts of these inclusions, the canonical functor from the fiber at op ⦋n⦌ to the product of the fibers at op ⦋1⦌ is an equivalence of category. One can thus interpret the objects of the fiber at op ⦋2⦌ as pairs of elements of the fiber at op ⦋1⦌, and the maps induced by the opposites of the two inclusions ⦋1⦌ ⟶ ⦋2⦌ might be thought of as the "source/target" maps. In this story, all the "coherences" are encoded in the simplex category.

The data of an "unbiased monoidal category" is then that of such a functor F which is a cocartesian fibration. Equivalently, this is the data of a certain pseudofunctor to Cat with certain properties. I formalized part of this story: you can see this thread: #mathlib4 > Coherence of higher arity tensor products in mon. categories . I never got to upstream this as I want to first get the (much harder) symmetric case (where SimplexCategory is replaced by the category of pointed finite types) first.

[Adrian Marti]

I'm actually familiar with Lurie's $\infty$-operads (symmetric case), and I actually thought about encoding a coloured operad in that way, thinking that it might simply things. However, in the end I didn't pursue the idea, because I felt like it was getting away from the spirit of what an operad is really supposed to be.

Also, while I have used operads in Lurie's sense throughout my master's thesis, I still feel some unease with it. It feels like kind of an accident that operads can be encoded in that way and not like a canonical construction. Maybe I'm just not seeing it.

[Adrian Marti]

The pseudofunctor perspective would make intuitive sense to me, but we can't really turn it into a pseudofunctor if not all arrows have cocartesian lifts, right?

[Robin Carlier]

Yes, if it’s not a full cocartesian fibration (i.e a monoidal category) then there’s no pseudofunctor.

[Robin Carlier]

The reason why I picked the $\infty$-framework when doing that was also because I thought as well it would minimize how much "coherence hell" you have to run into (all the coherences live in the simplex category), so you don’t have to play with flatten and such. I agree that this is a roundabout way of doing things, and that arguably, you lose the fact that there is a well-defined composition/tensor product (it gets "up-to-unique-iso-well-defined" by a universal property as some cocartesian lift instead).

An other reason why I went with this setup (which might legitimately not be interesting to you) is that I have high hope that some day Mathlib will have some $(\infty,1)$-category theory/"higher algebra" and when that happens there will be no way around proving that a "biased" monoidal 1-category is a monoidal infinity-category and at that point these kind of constructions will be needed anyways.

[Adrian Marti]

I genuinely think that the $\infty$-setting is really interesting, though higher algebra might be quite a big project to get going :wink:

[Kevin Buzzard]

You know about the #Infinity-Cosmos channel, right?

[Adrian Marti]

Yes! I don't know that there is a way to do higher algebra with $\infty$-cosmoi yet though. $\infty$-operads are weird.

[Adrian Marti]

Also: the flatten and single really come from the unit and multiplication the monad Assoc (which is the same as the list monad). My formalization is roughly guided by this nlab pagenlab page.

[Robin Carlier]

regarding the filling of some sorries in the code above: you'll have to assume that C is strict for ofMonoidal to go through, right? As far as I understand, you ask for strict associativity and strict unitality in your definition of a multicategory, and mathlib's MonoidalCategory are non-stricts.

[Adrian Marti]

Yeah, you're right it looks a bit fishy. Assoc.catProd is a construction that does not have the expected properties (strictly). Which is, I guess, something that you were trying to fix in your code in the link. Still, in a multicategory diagrams commute strictly and there is no such thing as 'commute up to iso' so I might get away with it :shrug: (don't know)

[Adrian Marti]

I've been looking at the unbiased approach to monoidal $\infty$-categories for a bit and I feel like some things have started to make sense. The opposite simplex category $\Delta^{op}$ classifies monoids with projections, in the following sense. It has a monoidal structure by glueing posets $[n],[m]$ to a poset $[n + m]$ along $n \in [n]$ and $0 \in [m]$. We also have a multiplication operation $d_1: [2] \to [1]$ and a unit $s: [0] \to [1]$ forming a monoid. Moreover, $d_0,d_2: [2] \to [1]$ are maps that we might think of as projection maps.

Given a monoidal category $\mathcal{C}$, a (strong) monoidal functor $F : \Delta^{op} \to \mathcal{C}$ now consists of a monoid $m$ in $\mathcal{C}$ together with some projection maps that turn out to be the usual projection maps when $\mathcal{C}$ carries the cartesian monoidal structure.

This means that it is actually quite natural to use $\Delta^{op}$ to define structures that are supposed to be monoids and even use it to encode all the higher coherences and additionally allowing for projections to occur in coherence diagrams. I believe a monoidal $\infty$-category should be precisely a monoidal (in some appropriate sense) $\infty$-functor $\Delta^{op} \to \textup{Cat}$. Or, we present this as a cocartesian fibration $\mathcal{C} \to \Delta^{op}$ satisfying the precise conditions ensuring that it preserves the monoidal structure.

We can do the exact same thing when replacing $\Delta$ with the Segal category $\Gamma$ and get the analogous constructions for the symmetric case (also with the additional projection maps).

Am I understanding this correctly?

[Robin Carlier]

So I think the idea that $\Delta^{\mathrm{op}}$ (with some added structure) classifies monoids is correct, but there are a few quirks. It is not a monoidal category with the structure you described: the formula works on objects, but has no obvious way to extend to morphisms (e.g what is $d_1^1 \otimes d_1^1 : [4] \to [2]$?). Instead the correct formula to get a monoidal structure is $[n] \otimes [m] = [n + 1 + m]$, but then $\Delta$ does not have a unit anymore, and so this is a monoidal structure on the augmented simplex category $\Delta_+$.

But that’s OK and instead you just have to keep track of this extra structure on $\Delta$ "by hand" and this is exactly what is achieved in Lurie by constructing a functor Cut from $\Delta^{\mathrm{op}}$ to the (category of operators of a model of the) associative operad. The assertion that "monoidal $\infty$-categories are some functors $\Delta^\mathrm{op} \to \mathrm{Cat}_\infty$" is then encoded in the fact that the map Cut is an "approximation of $\infty$-operads" (which is just pure combinatorics on $\Delta$ and $\mathrm{Assoc}$) and which has as a consequence that indeed monoidal $\infty$-categories (or, really, any kind of $Assoc$-algebra in any monoidal category) can be encoded as a simplicial object satisfying some properties.

And so yes: you can do the same things with $\Gamma$ instead! The "structure" for a category to work as some kind of "classifier" for algebraic objects is that of an "algebraic pattern": the article https://arxiv.org/abs/1907.03977 has some details.

[Adrian Marti]

Okay, so the story is not as simple as I thought. Indeed, it appears that I didn't really check what this product does on morphisms :pensive: . I don't think the monoidal category structure on the augmented simplicial category is actually useful for doing what I wanted to do (even though it is known to classify monoids), since the multiplication map of the monoid in there does not agree with the map that we lift in order to get the monoidal product in your definition of a monoidal $\infty$-category in the first comment: We want to consider the lift of $[2] \to [1]$, but he multiplication in $\Delta_+$ is the map $d_0:[1] \to [0]$.

I think that the Cut functor might be more along the lines of what I'm trying to do. But honestly, I'm also fine with saying that the segal map is an isomorphism. I just mistakenly thought it could be described by requiring the functor to be strong monoidal.

[Adrian Marti]

Back to the original topic though, I've been refining my formalization of coloured operads (maybe we should name them that way because this term is more commonly used than multicategory) and I am still not completely sure which approach is better and might suit mathlib's goals better:

• Operads through a type of arrows A and a type of objects O together with a source map A -> T O and a target map A -> O, where T is a variation of the list monad listing multiple inputs.
• A dependently typed approach, where we have a type of objects O and a type Mul (x,y) for each x : T O and y : O. Here enrichment (such as in vector spaces) is easier and the symmetric group action is also easier to describe (for symmetric operads). However, composition can be a bit more tricky (I think).
• There is also the fully unbiased approach "a la Lurie", but I believe that I want to be able to construct operads fairly easily and the approaches above might work better (I could be wrong though).

[Robin Carlier]

Yes, I’m also not entirely sure on how to make the fact that the augmented simplex category classifies monoids in that story, which is why I didn’t expand too much on this (my gut feeling is that there is a nice explanation for this).

[Robin Carlier]

I think the closest to the current approach to categories we have in Mathlib would be 2, but I agree with you that you will have to deal with some "DTT hell" with that approach, especially for defining composition.
A trick that is sometimes used (e.g when we deal with strict bicategories in Mathlib) is to give "definitional" control over some of the arguments by adding extra hyps of the form _ = _: e.g docs#CategoryTheory.Pseudofunctor.mapComp', where the type of the iso is "corrected" by an equality given as parameter. Maybe this would make composition slightly easier (at the cost of having to provide proofs that the family of targets of the first maps is the right family of source for the second map, but hopefully this can be handed over to automation).

[Adrian Marti]

This is a great idea! It had actually crossed my mind to define the composition for a morphism f : a -> b and a morphism g : c -> d and an equality b = c (so kind of similar to my current approach, but without loosing the dependent type). Perhaps there are some good options to be explored here.

[Calvin Lee]

Hi! these threads are interesting since im working a bit on multicategory/operad stuff for my phd. I'm specifically working in agda and the univalent case, since things are a bit more complicated there, but they should be easier in lean.

Is there anything wrong with using the classic (Burroni) T-categories, where you define a generalized multicategory as a monad in the bicategory of T-spans where T is a cartesian monad on sets?
afaik Lean already has (co)monads in a bicategory, so this wouldn't be a ton of work. you can also check out my WIP on the bicategory of T-spans here if it helps, and the 1lab proof that (lean style) categories are monads in the bicategory of spans on sets

[Adrian Marti]

The approach in the original post is heavily inspired by this idea that a multicategory is a monad in the category of T-spans, as described here. However, there are a couple finer points.

• I don't want to overuse abstraction, since I do think that it can have its drawbacks. I feel like it can create a disconnect between what is commonly thought of as an operad and what is actually written in code, possibly confusing users and alienating the mathlib community. I find it reasonable to define multicategories depending on a cartesian monad T, which then controls whether we're in the planar, symmetric or even cartesian case. This is elegant, however, I wouldn't go the extra step of using T-spans.
• Top-down abstract nonsense definitions do also the drawback that it is not immediately clear what the data is behind the operad. This means that even composing two arrows would require constructing an element in some composition of T-spans which is some pullback, which is indirection that will slow you down when working with examples of operads.
• If you want to use T-spans for the symmetric and the cartesian case, T must be allowed to be a monad on Cat and you have to have both functors in the T-span to be discrete fibrations, to model the permutation action.
• It's hard to enrich the multicategory over vector spaces, which is a common application.

[Adrian Marti]

Instead of working with spans, we can work with the category of categories, together with profunctors (these are functors Prof C D := Cᵒᵖ x D -> Set) and a suitable notion of monad on this (there seems to be necessary extra structure on the monad, see this paper). This yields a different way to formalize multicategories, where we do have the usual type of multiarrows Mul(X,Y). This can be easily enriched in vector spaces and the symmetric and cartesian case work more naturally. It might have other drawbacks.

[Calvin Lee]

you don't need to explain what a profunctor is.

The Cruttwell-Shulman definition depends on virtual double categories, which, in my opinion already capture much of the interesting structure of a multicategory, so it doesn't make sense to start there. I agree there's no need to have needless abstraction, but i like starting with the Cartesian monad since this and the composition operation in Span abstract many of the difficult transports that you mentioned.

but also agree about T having to be a monad (or something similar) on Cat. This is essentially what stops the T-spans thing from working in homotopy type theory. I've been looking more at the Lurie definition recently for this reason

[Adrian Marti]

Yeah, I agree it makes no sense to start with virtual double categories. And also, you're right that the transports become easy with the T-span approach. At the end of the day, this is an experiment in figuring out what works.

I actually have a formalization of multicategories in terms of spans (not T-spans) and parameterized in a cartesian monad T (Multicategory.lean). I didn't generalize it to Cat yet, since I was still figuring out how to state the equivariance conditions using fibrations on pen and paper. Now I'm trying the profunctor approach to compare.