ct.category theory - Lax and Colax Monads

This isn't technically an answer, but depending on your examples, you might want to think about lax/colax monads on (pseudo) double categories instead. Part of the problem with lax monads on bicategories is that there is no tricategory of bicategories and lax functors, whereas there is a 2-category of pseudo double categories and lax functors, so that all of the "formal theory of monads" can be applied directly to lax monads on double categories. Most of the lax functors and lax monads that I've seen on bicategories have "actually" lived on double categories, except that people tend to forget about the extra direction of arrows and think only about the bicategory.