Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Ah, I hadn't realised that about pseudofunctors. It makes sense intuitively, but is there a simple proof of that fact? For a non-universal embedding, what I have in mind is that every monoidal category embeds fully faithfully in a left-closed monoidal category via Yoneda and Day convolution. Therefore a local bicompletion should embed a bicategory locally fully faithfully into a left-closed bicategory. I think one wants left-coclosure here, so probably one needs to take the local completion instead, but it seems like everything ought to work out.
For the problem I am interested in, it should suffice to find any faithful locally fully faithful pseudofunctor into a bicategory admitting all left extensions. It seemed neatest to do so universally, but this is not actually important. Perhaps there is an easier solution in this case.
@TimCampion: that's an interesting approach. Coherence of the double involution on ∗-autonomous categories gives a coherence result for (symmetric) *-autonomous categories. Perhaps this can be reflected to give one for symmetric closed monoidal categories (it certainly provides further evidence that a coherence theorem holds).
I'm reasonably sure it is true, and think I can prove it using a syntactic argument, but there are quite a number of conditions to check, and I would hope there was either a more elegant argument, or a proof already in the literature.