[Math] tricategory of bicategories and biprofunctors

Question

Background

There is a bicategory where the objects are categories, the 1-morphisms are profunctors, and the 2-morphisms are morphisms of profunctors. The non-obvious part of this assertion is that profunctors admit a "good" (i.e., coherently associative) composition. The way one sees this is to use the fact that the Yoneda embedding is the free cocompletion, from which we may identify profunctors from $\mathcal{C}$ to $\mathcal{D}$ with cocontinuous functors from $\operatorname{Set}^{\mathcal{C}^{\operatorname{op}}}$ to $\operatorname{Set}^{\mathcal{D}^{\operatorname{op}}}$. Over here, there is a strictly associative composition, so life is good.

All of this extends easily to the enriched setting. In particular, if we enrich over $\mathcal{V} = \operatorname{Cat}$, we can talk about strict 2-profunctors between strict 2-categories, and we get a nice bicategory of 2-categories, strict 2-profunctors, and morphisms between these.

Question

I would like to know if there is an analogous way to obtain a tricategory of bicategories and biprofunctors. You can "follow your nose" and write down what the composition should be, but checking all the axioms of a tricategory does not seem like the simplest approach. Of course, we can strictify to get equivalent strict 2-categories and 2-profunctors, but I doubt the composition will be the same; I don't think the "strict" colimits will in general agree with the "weak" colimits. Also, using the standard enriched theory only gives a bicategory; the natural transformations are lost. It seems that an appropriate statement of the form "the bicategorical Yoneda embedding is a free cocompletion" will handle things just as it does in the setting of ordinary profunctors, but I am not sufficiently comfortable with limits and colimits in bicategories to try to figure out if such a statement makes sense. Has anybody worked all of this out?

(The closest thing I have seen to such a result is Justin Greenough’s paper Monoidal 2-structure of Bimodule Categories, which more or less establishes this result in the case of sufficiently nice $k$-linear monoidal categories. But his proof seems to be very specific to that setting, whereas one would hope that a proof could be established along the same lines as the result for usual profunctors.)

Answer 1

For those coming across this question more recently, there is now an answer to the original question. In fact, the tricategory of pseudoprofunctors has been defined twice, independently, via different approaches.

• Lawler defines the tricategory $2\text{-}\mathbb P\mathrm{rof}$ of bicategories and pseudoprofunctors (there called "2-profunctors") in Definition 4.1.1 of his 2014 thesis Fibrations of predicates and bicategories of relations. The hom-bicategories are given by the cocontinuous pseudofunctors between cocomplete bicategories, which is justified as corresponding to pseudoprofunctors by the results of Section 3.2.3. Defining the hom-bicategories in this way guarantees the coherence conditions hold immediately.
• Chikhladze defines the tricategory $2\text{-}\mathcal P\mathrm{rof}$ of bicategories and pseudoprofunctors (there called "biprofunctors") in Section 8 of his 2014 paper Lax formal theory of monads, monoidal approach to bicategorical structures and generalized operads. Here, the approach taken is to define a bicategorical $\mathrm{Mat}$ construction, along with a bicategorical $\mathrm{Mod}$ construction, so that $2\text{-}\mathcal P\mathrm{rof} = \mathrm{Mod}(\mathrm{Mat}(\mathrm{Cat}))$. That $2\text{-}\mathcal P\mathrm{rof}$ is a tricategory then follows from the coherence of simpler constructions, which are shown to coincide with pseudoprofunctors in the same way as in the 1-categorical setting.