Given a bicategory $\mathcal K$, is there a universal construction of a bicategory $\mathcal K'$ and faithful locally fully faithful pseudofunctor $\mathcal K \hookrightarrow \mathcal K'$ such that for each pair of 1-cells $f : A \to B$ and $g : A \to C$ in $\mathcal K$, the left extension $\mathrm{lan}_f g : B \to C$ exists in $\mathcal K'$? That is, is it possible to freely adjoin left extensions for every pair of 1-cells with common codomain?

If there is not an explicit construction (in the literature or elsewhere), I would be happy for a demonstration that a construction exists. I suspect one can prove that a syntactic construction works, but I would rather avoid trying this if there is a more elegant approach.

A related question regards adjoining adjoints to 1-cells in bicategories, for which a partial solution can be found in Dawson–Paré–Pronk's Adjoining adjoints.

existenceof a universal such functor $\mathcal{K} \to \mathcal{K}'$, and for that functor to be locally fully faithful, are two very different things. The former should be just an exercise in 2-dimensional universal algebra; the latter is more of a coherence / cut-elimination result that would probably require a more careful syntactic-like analysis of the particular situation. Which statement are you more interested in? $\endgroup$2more comments