2-monads for categories with a class of (co)limits

Question

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.

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.