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.

- 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.
- 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?
- Similarly, is it known whether the small cocompletion of locally-small categories forms a 2-monad?
- 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.

specified$\phi$-limits, and 1-cells whichstrictlypreserve 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 '20 at 14:19