Strictness of two operations on proarrow equipments

Question

There are several equivalent definitions of a profunctor between categories $C$ and $D$. I'm interested in the following two:

1. A functor $C\times D^o \to \text{Set}$
2. A co-continuous functor between presheaf categories $\hat C \to \hat D$

These are equivalent by the free co-completion property of the Yoneda embedding.

The advantage of definition 2 is that the composition of profunctors is strictly associative/unital (just functor composition) whereas composition using definition 1 is only weakly associative/unital.

However it seems to me there is a corresponding advantage to definition 1. If we are interested in the pro-arrow equipment of categories/functors/profunctors/natural transformations, then we also use the operation of restriction of a profunctor $R : C \not\rightarrow D$ along functors $F : C' \to C$ and $G : D' \to D$ giving us a profunctor $R(F,G) : C' \not\rightarrow D'$. By definition 1, this operation is strictly associative in that $$R(F\circ F',G\circ G') = R(F,G)(F',G')$$ $$R(\text{id},\text{id}) = R$$ However, I don't see a way to define this operation for definition (2) that is strictly associative.

So my questions are

1. Is there a way to define restriction of co-continuous functors that is strictly associative?
2. Either way, is there a theorem showing that every pro-arrow equipment with weakly associative composition and restriction is equivalent to one where both composition and restriction are strictly associative/unital?

Answer 1

I believe the answer to (2) is yes.

First, apply the strictification theorem for bicategories twice, to make composition of arrows and proarrows both strictly associative. Thus, when our equipment is regarded as a double category, we have a strict double category. (We could also probably apply some coherence theorem for double categories directly, as Kevin Arlin suggested in a comment.)

Second, recall that the restriction of a proarrow $R:C \nrightarrow D$ along arrows $f:C'\to C$ and $g:D'\to D$ can be defined/constructed as $f_\bullet \odot R \odot g^\bullet$, where $f_\bullet$ is a companion of $f$, and $g^\bullet$ is a conjoint of $g$. Thus, if companions and conjoints can be chosed strictly functorially, the strict associativity of composition of proarrows will give strict functoriality of restriction.

Now redefine an "arrow" $f:C'\to C$ to consist of an arrow in the original (strictified) sense together with a chosen companion and conjoint. Since a composite of companions (resp. conjoints) is a companion (resp. conjoint) of the composite, and companions and conjoints are essentially unique, this is equivalent to the original 2-category of arrows. But now it admits a strictly functorial choice of companions and conjoints.

If we apply this construction to cocontinuous functors, we get a notion of "strictly functorial restriction" for them, but at the cost of fattening up the notion of "functor". We don't have to fatten it up quite as much, since with cocontinuous functors we automatically get a strictly functorial choice of conjoints, namely precomposition, but we do have to equip each functor with a chosen left Kan extension to presheaves to be the companions. It's possible there is some trick that can do better than this, but I don't know what it is offhand.