This question concerns the strictness of (co)completions, at various levels of generality.

In Blackwell–Kelly–Power's Two-dimensional monad theory, the authors state

For instance, the 2-category $\mathbf{Lex}$ of small finitely-complete categories, left-exact functors, and natural transformations is (see Subsection 6.4 below) $T\text{-}\mathbf{Alg}$ for a finitary 2-monad $T$ on Cat.

  1. Where can be found an explicit proof that there is such a 2-monad, as opposed to a pseudomonad? This claim appears in several other papers, but I have only been able to find constructions of a pseudomonad for finite limit completion.
  2. More generally, is there an explicit proof in the literature that, for a suitable class $\phi$ of (co)limits, there is a 2-monad on $\mathbf{Cat}$ for $\phi$-(co)completion, whose algebras and (pseudo)morphisms are $\phi$-(co)complete categories, $\phi$-(co)continuous functors, and natural transformations?
  3. Similarly, is it known whether the small cocompletion of locally-small categories forms a 2-monad?
  4. Most generally, are there any results that establish when a lax idempotent pseudomonad (i.e. KZ-doctrine) on a 2-category $\mathcal K$ may be replaced by a lax idempotent 2-monad on $\mathcal K$ (with isomorphic or equivalent 2-categories of algebras)?

Power–Cattani–Winskel's A Representation Result for Free Cocompletions in particular seems promising, but the characterisation result there still assumes that such 2-monads exist in the first place.

  • $\begingroup$ For (1), let $Cat_{\phi,s}$ be the 2-category of categories with specified $\phi$-limits, and 1-cells which strictly preserve these. It's supposed to be obvious that the forgetful functor $Cat_{\phi,s} \to Cat$ is strictly 2-monadic. You can construct the 2-monad via generators and relations just like in universal algebra. That said, I don't know where this has been done explicitly. For (2), you will need to take pseudo-morphisms to "undo" the extra strictness gotten by working with this 2-monad. $\endgroup$
    – Tim Campion
    Sep 23, 2020 at 14:19
  • $\begingroup$ Thanks. The construction via a (2-categorical) presentation was the one I had in mind, but that taking pseudomorphisms instead of strict morphisms suffices to obtain exactly the continuous functors seems a little subtle, which is why I would have liked to seen it proven. Additionally, if this construction works for, say, finite completion, I see no reason it would not also work for small completion (with an appropriate notion of large presentation), but several people have expressed to me they would be surprised if the small cocompletion pseudomonad could be strictified into a 2-monad. $\endgroup$
    – varkor
    Sep 23, 2020 at 15:20

1 Answer 1


Kelly and Lack's paper On the monadicity of categories with chosen colimits answers your questions (1),(2) and (3) affirmatively. The main theorems are Theorem 6.1, 6.2 and 7.1. Their main trick is Lemma 4.1, which allows them to modify a biadjunction (and so a pseudomonad) to a strict 2-adjunction (and so a 2-monad), assuming various hypothesis. I can imagine that something like this lemma might be helpful also in answering you question (4), but I am not aware of seeing any result of that nature.

Regarding your comment on presentations: if you have any presentation for a 2-monad (for instance, for categories with finite limits) and want to check that its pseudomorphisms are the expected ones (in this case, finite limit preserving functors), it is enough to know that those expected morphisms satisfy some natural properties such as doctrinal adjunction (so you don't have to work with the presentation at all). This is described in my paper Two-dimensional monadicity, with your example discussed in Section 7.2.

  • $\begingroup$ Thank you, both of those references are perfect! $\endgroup$
    – varkor
    Sep 23, 2020 at 17:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.