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

- A functor $C\times D^o \to \text{Set}$
- 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

- Is there a way to define restriction of co-continuous functors that is strictly associative?
- 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?