distributive law of monads

Stream: maths

[Sina Hazratpour 𓃵]

I could not find this on mathlib. Is there work on distributive law of monads off mathlib that can be PRd? Otherwise, I'm happy to work on it, as I need the distributivity of the bag monad over the list monad.

[Yaël Dillies]

I had vague plans to formalise them (a friend and I last summer figured out a way to create many distributive laws between two specific monads), but they never concretised. I would love if you worked on that!

[Sina Hazratpour 𓃵]

I can start with a minimal PR today. You are very welcome to help. :)

[Yaël Dillies]

I am afraid I am still 5 refactors deep into the todo list :sweat:

[Sina Hazratpour 𓃵]

no worries.

btw, I can also imagine there can be some design choices in terms of the level generality. Street's formal theory of monads for example is an abstract but elegant way of dealing with the distributivity law, but it is 2-categorical.

[Sina Hazratpour 𓃵]

https://ncatlab.org/nlab/show/monad#BicategoryOfMonads

[Nicolas Rolland]

I am interested in helping, my level of Lean permitting.

In theory, it would be interesting to start with morphism in Endo(Cat), which is a sub-2category of Cat//Cat.

Cat//Cat is the 2-category whose morphism are lax-squares of Cat (otherwise called Quintet(Cat)). Objects are functors, arrow are triple of a functor joining the domains, a functor joining the codomains, and a natural transformation between them. There are obvious 2-functors dom and cod to Cat, and it is a really a span in 2-Cat

Endo(Cat) is the sub-2-category whose objects are endofunctors and whose morphisms are a pair a single functor for the domains and codomains and a natural transformation

Mon(Cat) is the sub-2-category of Endo(Cat) verifying the additional monad morphisms conditions

This whole machinery works for 2-categories other than Cat obviously.
So it would be best to describe that 2-categorically for some 2-Cat K

[Sina Hazratpour 𓃵]

I feel Street's machinery is along the same lines but for any 2-category/bicategory $\frak{K}$. My inclination for now is to formalize the distributive law just for categories and monads of categories and do the Street's 2-categorical construction separately maybe in the bicategory library. I wonder what maintainers think about this.

[Yaël Dillies]

Not a maintainer but this sounds like a reasonable (and usable!) approach

[Yuma Mizuno]

@Sina H 𓃵 For 2-categorical approch, I have this draft PR #14889, which formalize the bicategory of comonads. I'm not sure I can open this PR in the near future, I think it has some thing to do with you way.

[Sina Hazratpour 𓃵]

@Yuma Mizuno Thanks, I'll have a look.

[Nicolas Rolland]

I don't have enough lean experience to know how much more complex (or simple, that's what good abstractions are about ! ) it can be in Lean.

That said, I imagine that having a formalisation in Cat should only help the 2-categorical approach : only primitive notions are involved, so they can be unplugged later for more general K.

[Sina Hazratpour 𓃵]

sure, that seems a good test case. If you think doing it in Cat is significantly easier than directly doing it in a bicategory, then I think it might be good to start there and later abstracted away to bicategories. But note that at the end the bicategory one should go to mathlib since there are interesting examples of monads which are not functors: for instance a monad in the bicategory of spans is an internal category.

[Nicolas Rolland]

No doubt monads in bicategory are interesting.

What I was hinting at is that expliciting the intermediate structures K//K, Endo(K), Mnd(K) is useful, as interesting phenomenas happen at those levels. For instance, it helps to rephrase the comparison functor of G |- F as the 2-cell G -(G,id)-> GF left adjoint (in K//K !!) to the trivial 2-cell GF - (F,id)> G.