In the prominent examples of weak double categories (or bicategories), the weak composition is typically defined by a universal property (specifically, it's usually the tensor product of some kind of bimodules), and as such it's not a uniquely designated arrow.  

However, the currently accepted definitions also require *specific assignments* as the weak composition, and impose the coherence axioms on them.


Is this question treated in the literature?


I suggest to simply replace the 'specific assignments', i.e. the functor which is performing the weak composition by a *functorial profunctor*.  

What would then happen to the coherence axioms?




---


Let me spell out a possible start:


Let $Gr(C)$ denote the category of internal directed graphs of a category $C$ (i.e. diagrams of two parallel arrows), and let $P:Gr(C)\to Gr(C)$ be the '*path monad*' which assigns the graph with the same vertices and all paths of the original graph as edges to an arbitrary graph.  

An internal category is just an algebra for this monad $P$:  

That is, it's a graph $G:E\overset{s,t}\to V$ equipped with a 'composition' $c:P(G)\to G$ that behaves appropriately with the monad structure.


Specifically, if $C=Cat$, we arrive to strict double categories, and the composition is ultimately (determined by) a *functor* $c:E\_{P(G)}\to E$.  

So, instead of a functor, what would happen if we considered the weak composition operation as a (functorial) profunctor $c':E\_{P(G)}\not\to E$?  

[A profunctor $u:A\not\to B$ is a functor $u:A^{op}\times B\to Set$, it's functorial if $u(a,-)$ is representable for each object $a\in A$. Note however, that there are no single representing objects designated in $B$ for objects of $A$.]


Finally, a naive question:  

Isn't it possible that if the conditions of being a $P$-algebra could be properly translated in this setting, then we can get rid of the coherence axioms for the weak composition?



Proper weakness condition of double categories
There's a general theory of this sort of "replacing algebraic structure by universal properties", called [generalized multicategories](https://ncatlab.org/nlab/show/generalized+multicategory). The simplest case is for an ordinary monoidal category, in which case the corresponding "virtual" structure is a [multicategory](https://ncatlab.org/nlab/show/multicategory), which has "multi-maps" in terms of which the tensor product can be characterized by a universal property. The analogous thing for a double category is known as a [virtual double category](https://ncatlab.org/nlab/show/virtual+double+category). The general notion of generalized multicategory is quite similar to your sketched idea in terms of a "pro-algebra" for a monad.


