Strictification of 2-monads

Research
1

I have been thinking about strictness recently, because it matters for implementation, and I think I have a “nicer” way of doing monoidal categories and symmetric monoidal categories.

In programming languages, we often have a notion of tuple type. For instance, in Julia we have Tuple{A,B,C...}. Modeling this as a monoidal structure on the category of types in the traditional way, where we have a binary operation and a unit, and then associators and unitors, doesn’t actually fit what’s going on, because we have native n-ary operations.

Instead, we could model this as an algebra of the list 2-monad \mathrm{List} \colon \mathsf{Cat} \to \mathsf{Cat}. The list monad sends a category \mathsf{C} to the category \mathrm{List}(\mathsf{C}), where an object is a pair (n \in \mathbb{N}, \{X_i \in \mathsf{C}\}_{i \in \{1,\ldots,n\}}), and a morphism from (n, \{X_i\}) to (n, \{Y_i\}) is a choice of maps f_i \colon X_i \to Y_i (there are no morphisms (n,\{X_i\}) \to (m,\{Y_i\}) for n \neq m).

This is a monad essentially because we can collapse lists.

This models our Tuple operation: we take a list of types, and we get a type.

However, this is not a strict algebra, because Tuple{A, Tuple{B,C}} is not equal to Tuple{Tuple{A,B},C}, even though flatten [[1,2],3] == flatten [1,[2,3]].

One thought I had was to instead model this as a strict algebra of \mathrm{List}^\ast, the free monad on the list 2-monad. \mathrm{List}^\ast sends a category \mathsf{C} to the category where an object is a tuple (t, \{ X_i \}_{i \in \mathrm{leaf}(t)}), where t is an arbitrary nesting of the list [1,\ldots,n] for some n. I.e., [1,[2,[3],[[4]]]] or something. This allows the 2-monad to “remember” the nesting, and thus we can have a strict algebra without forcing Tuple{A,Tuple{B,C}} to be equal to Tuple{Tuple{A,B},C}.

However, this doesn’t give us any associativity properties; any functor \mathrm{List}(\mathsf{C}) \to \mathsf{C} automatically gives us an algebra of \mathrm{List}^\ast.

So instead, we do something sneaky. We modify \mathrm{List}^\ast to say that the morphisms between (t,\{X_i\}) and (t',\{Y_i\}) are collections \{f_i \colon X_i \to Y_i\} even when t \neq t', as long as t and t' flatten to the same list. This means that there is a canonical morphism between any two nestings of the same list given by f_i = \mathrm{id}_{X_i}. With this modification, \mathrm{List}^\ast(\mathsf{C}) is equivalent to \mathrm{List}(\mathsf{C}), but not isomorphic. Then Tuple forms a strict algebra of \mathrm{List}^\ast!

I think, but I’m not sure, that this is an instance of a general construction where pseudo-algebras of a 2-monad are equivalent to strict algebras of another 2-monad; I remember seeing something like this in A 2-categories companion but my 2-fu is not strong enough yet to be fully fluent with this stuff.

Anyways, I like this way of doing monoidal categories because I think it captures more faithfully how people actually use monoidal categories in practice, with unbiased operations like A \otimes B \otimes C.

I also think that we can do a similar construction for symmetric monoidal categories where we modify \mathsf{List}^\ast to say that the morphisms between (t,\{X_i\}) and (t',\{Y_i\}) are pairs of permutations \sigma \in S_n and morphisms \{f_i \colon X_i \to Y_{\sigma(i)}\}.

I also want to model more carefully the operation of NamedTuple and the operation of struct creation, but that will have to wait for another day.

2

Mike Shulman has a paper Not every pseudoalgebra is equivalent to a strict one where he describes a a finitary 2-monad on a locally finitely presentable 2-category for which not every pseudoalgebra is equivalent to a strict one. But there are positive results, and some are discussed in Alex Corner’s blog article, where he describes a “Theorem-Schema” that covers some ways of showing every pseudoalgebra is equivalent to a strict one.

One of the simplest is by Power, who showed every pseudoalgebra for a 2-monad T on Cat is equivalent to a strict one if T has this property: if a functor F is bijective on objects, so is T(F). This handles a bunch of cases. For example, it implies every monoidal category is equivalent to a strict one.

Power’s theorem also works for powers of Cat, so it also gives a way to strictify bicategories.

1 Like
3

A complication with this case is that you want to replace a 2-monad T, which is not itself an algebra for a 2-monad on Cat. But it is an algebra for the “free monad monad” on the 2-category of endo-2-functors of Cat. (Say that three times fast!) (And maybe I just want accessible endo-2-functors or something.) And if you replace T, seen as an algebra, with a T' such that pseudo-maps of 2-monads out of T are the same as strict maps out of T', then in particular strict algebras for T' are the same as pseudo-algebras for T. Why? Because pseudo-maps of 2-monads out of T contain pseudoalgebras TA\to A for T in the form of maps T\to \langle A,A\rangle where the codomain is some 2-monad generated by A.

It seems like this general construction is of less interest than the observation that you can just write down T' explicitly in practice, though, as Owen did here.

4

Let’s see if I can break this down for anyone who didn’t have the benefit of this being explained in person by Kevin as well…

The free monad monad on the 2-category of endo-2-functors of Cat sends an endo-2-functor to the free 2-monad on that endo-2-functor. My intuition for this is that if an endo-2-functor describes the “operations” that you can do on a category, then the free-2-monad describes “syntax trees of those operations”. An algebra for the free monad monad then tells you how to compose a syntax tree of operations into a single operation. I.e., how to “flatten” a nested operation. So this checks out; an algebra for the free monad monad is a 2-monad! Neat.

Then the second interesting thing here is that an algebra of a monad T is the same thing as a map T \to \langle A, A \rangle, and moreover the algebra being weak/strict is equivalent to the map being weak/strict. I vaguely remember reading about this in Lack, but I’m glad to relearn this. This is nice because it allows algebras to be talked about using normal 2-category theory, for instance talking about the “pseudo map classifier”, i.e. a 2-monad T' which “represents” pseudo maps in the sense that there is a natural bijection between strict maps out of T' and pseudo maps out of T. This is a slick way to phrase the construction I was interested in.

5

Perhaps this is straying a bit far from the original point, but I just realized from Kevin’s comment that this is an example of something I’m familiar with :slight_smile: Generally when you have algebras with a notion of strict vs pseudo vs lax etc morphisms, each non-strict type of morphism can be modeled as coKleisli arrows for some “relaxation” comonad on the algebras.

For instance, lax monoidal functors A → B correspond to strict monoidal functors LA → B, where (LA,x) is the free monoidal category on A with the coherent lax structure maps a x b → ab added in. L is a comonad, typically defined as “take the free thing then add in some extra coherences”. Similarly pseudofunctors A → B between 2-categories correspond to strict 2-functors LA → B where LA looks like the free category on A on the 1-cells with coherences natural with respect to the 2-cells.

In this case, going from T to T’ should also be a comonad and like you said T’ is built by adding in extra coherence operations to the free monad on T. Pseudo-maps from T corresponding to strict monad maps from T’ fits this form perfectly.

1 Like
6

Going one level down I guess, I’m pretty sure there is not a “free monad” monad, sending any endofunctor on any category to a “free monad on that functor”. The reason is that the forgetful functor from the 2-category of categories-equipped-with-monad to the 2-category Cat has no left adjoint, ultimately for size reasons. I’m having trouble finding a proof; the closest thing I can quickly find is the discussion here:

I got Todd Trimble to explain this to me once, but maybe that conversation is on the nForum.

7

But what about the forgetful functor from the category of monads on a fixed category \mathsf{C} to the category of endofunctors on that same category? I think that would be the analogous situation. The existence of such a left adjoint might depend on the category \mathsf{C}, but I think it certainly exists in some situations.

I agree that allowing both the category and the endofunctor to vary might get you in trouble with size issues.

8

Hmm, it’s true that’s a less ambitious question that might be more likely to have a positive answer, but I’m still dubious. Let’s dive in! Take \mathsf{C} = \mathsf{Set} for example, and try to build the free monad on an endofunctor F: \mathsf{Set} \to \mathsf{Set}. This is a special case of building the free monoid on an object in a monoidal category, so I immediately turn to Steve Lack’s paper Note on the construction of free monoids. He gives a quite general construction, but says

This case includes the free monoid, the free ring (on an additive abelian group), the free category (on a graph) and the free differential graded algebra (on a chain complex), but it does not help with the case of free monads. Conditions for the existence of free monads were given by Barr in [2].

[2] is this paper:

The link leads to the evil Springer: this is not open-access and I’m too lazy right now to gain access. There’s an open-access followup:

It’s deep but it confirms my suspicion that size issues are relevant: it involves some heavy-duty transfinite induction. I suspect the first paper would be easier to understand!

Or, you can try what I was originally going to try: just try to build the free monad on an endofunctor F: \mathsf{Set} \to \mathsf{Set} “by hand”, and see what happens!

9

Let’s see…

If F is an arbitrary functor, define T_F by letting T_F(A) be the colimit of

A \to A + F(A) \to A + F(A + F(A)) \to \cdots

As far as I know, this is a perfectly good colimit, no size issues. This is the least fixed point of B \mapsto A + F(B); I’m going to try and remember part of the proof of this.

There is a natural map T_F(A) \to A + F(T_F(A)) given by applying the universal property to the maps

A \to A + F(T_F(A)), A + F(A) \to A + F(T_F(A)), …

which are defined using the injection maps from the definition of colimit. Then I think we can show that this map is in fact an isomorphism, but it’s escaping me exactly how we do this.

if we manage to do this though, we get maps A \to T_F(A)) (the unit) and F(T_F(A)) \to T_F(A), which we can use to construct maps

T_F(A) \to T_F(A), T_F(A) + F(T_F(A)) \to T_F(A), T_F(A) + F(T_F(A) + F(T_F(A))) \to T_F(A), \ldots

that assemble into a map T_F^2(A) \to T_F(A) which is the multiplication.

Because \mathsf{Set} is closed under countable colimits, I don’t think that size issues are a problem here; I think there really is a free monad monad.

10

Then I think we can show that this map is in fact an isomorphism, but it’s escaping me exactly how we do this.

That could be exactly the problem that forces people into transfinite induction and the like. If F preserves colimits it’s probably easy to show this map is an isomorphism - right? But in general F won’t.

You’re trying to find a fixed point, right? (That is, a fixed point up to isomorphism.) And the way people find a fixed point is by iterating and hoping the answer converges. You’re hoping that iterating a countable number of times is good enough, but I’m pretty sure that’s not true in general. This is where size issues tend to come in. That’s why the articles I pointed you pull tricks like iterating up to a regular cardinal. But as the nLab points out, there is a free monad on any finitary endofunctor on \mathsf{Set}!

11

OK, I’m glad I know exactly where the size issues come into play then. I’m starting to get a better intuitive sense for what size issues mean in terms of computer implementation, so I have more respect for size issues as not just logician business.

12

It’s not hard to see how preserving filtered colimits leads to the existence of a free monad, because the free monad is built out of a filtered colimit, and then that allows you to show that F(T_F(A)) is the colimit of

F(A) \to F(A + F(A)) \to F(A + F(A + F(A))) \to \cdots

which lets you build the morphism F(T_F(A)) \to T_F(A) that you need.

The nlab says that finitary endofunctors on Set are completely determined by their values on all finite ordinals. I suppose this is because any infinite set can be built out of a filtered colimit of finite sets, specifically the filtered colimit of the lattice of all finite subsets of that infinite set.

OK, it all clicks into place! Neat, I now know why people care about finitary monads.

Next questions: what are examples of non-finitary monads, and what is the analogous 2-condition for 2-monads!

13

The nLab says that finitary endofunctors on Set are completely determined by their values on all finite ordinals. I suppose this is because any infinite set can be built out of a filtered colimit of finite sets, specifically the filtered colimit of the lattice of all finite subsets of that infinite set.

That sounds exactly right. “Filtered colimits” always seemed obscure and technical to me until I started thinking about the key example: the union of a increasing sequence of subsets of a set. That helped me see how lots of functors preserve filtered colimits but not arbitrary colimits. For example it’s good to check that the functor from \mathsf{Set} to \mathsf{Set} sending any set S to \mathrm{hom}(X,S) preserves filtered colimits iff the set X is finite. It’s wonderful to see how the concept of “finite” pops out here, seemingly out of thin air!

More generally an object X of any category is called compact if \mathrm{hom}(X,-) preserves filtered colimits. For example a group is compact in this sense iff it’s finitely presentable, and a topological space is a compact object in its poset of open subsets iff it’s compact in the usual sense.

Next questions: what are examples of non-finitary monads…

An algebraic gadget with infinitary operations obeying equational laws may well be an algebra of some non-finitary monad. For example there’s a finitary monad on \mathsf{Set} whose algebras are semilattices: commutative monoids where the monoid operation \vee obeys x \vee x = x. But there’s an infinitary monad on \mathsf{Set} whose algebras are \sigma-semilattices: these are a more powerful form of semilattice where you also have an operation of countably infinite arity

\bigvee_{i = 1}^\infty \; x_i

For example any \sigma-algebra gives a \sigma-semilattice if we take \bigvee to be \bigcup. There is also an infinitary monad whose algebras are complete semilattices, also called suplattices: these have operations of arbitrary arity

\bigvee_{i \in I} x_i

Here we start running into size issues: because the index set I can have arbitrary cardinality, there is actually a proper class of operations! But the monad for suplattices is very important: it’s the covariant power set functor P: \mathsf{Set} \to \mathsf{Set}, sending any set S to 2^S.

14

Late reply but the analogous condition on a 2-monad is still “preserving filtered colimits.” Nothing interesting changes about the nice properties of filtered colimits, unlike general colimits, when you start enriching over some fancier category. (There’s some paper on V-presentable categories by some superset of a subset of Kelly, Street, and Day making this claim specific.)

Incidentally, it’s not strictly filtered colimits, but “\lambda-filtered colimits for some \lambda” where \lambda might be a big cardinal and filtered colimits correspond to \lambda=\aleph_0. For instances the monad lattices with countable sups preserves \aleph_1-filtered colimits but, for all sups, no filtered colimits at all. I doubt the bigger \lambda s are ever relevant on the computer but you do start to see \lambda a lot if you read the literature on these kinds of issues.