# Strictness of two operations on proarrow equipments

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?
• Not an answer, but it smells to me like doubly weak double categories are the pseudo-algebras for a 2-monad on some kind of 2-category of double graphs whose strict algebras are strict double categories, and then the general coherence result should probably apply (though it sometimes fails for strictifying algebras, this seems like a very nice case.) Commented May 17, 2022 at 17:51

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.