Where is it rigorously stated and proved that the definition of lax functor implies that the generalized cocycle condition holds for an arbitrary number of composable $1$-cells?

Question

Let $\mathcal{A}$ and $\mathcal{B}$ be two $2$-categories and $F : \mathcal{A} \to \mathcal{B}$ be a lax $2$-functor. Given $1$-cells $(f_{i})_{0 \leq i \leq n}$ of $\mathcal{A}$ such that the composition $f_{n} \circ f_{n-1} \circ \cdots \circ f_{0}$ makes sense, this data together with the structural $2$-cells of $F$ give many paths of $2$-cells going from $F(f_{n}) \circ F(f_{n-1}) \circ \cdots \circ F(f_{0})$ to $F(f_{n} \circ f_{n-1} \circ \cdots \circ f_{0})$, for instance $$ F(f_{n}) \circ F(f_{n-1}) \circ \cdots \circ F(f_{0}) \Rightarrow F(f_{n} \circ f_{n-1}) \circ F(f_{n-2}) \circ \cdots \circ F(f_{0}) \Rightarrow \cdots $$ $$\Rightarrow F(f_{n} \circ f_{n-1} \circ \cdots \circ f_{0}) $$ and $$ F(f_{n}) \circ F(f_{n-1}) \circ \cdots \circ F(f_{0}) \Rightarrow F(f_{n}) \circ F(f_{n-1}) \circ \cdots \circ F(f_{1} \circ f_{0}) \Rightarrow \cdots $$ $$\Rightarrow F(f_{n} \circ f_{n-1} \circ \cdots \circ f_{0}) $$ which correspond to what one gets by "parenthesizing on the left" and "parenthesizing on the right" respectively. It seems to seem obvious that it follows from the definition of lax functor that the $C_{n}$ ways to parenthesize the left hand side all give the same $2$-cell $$ F(f_{n}) \circ F(f_{n-1}) \circ \cdots \circ F(f_{0}) \Rightarrow F(f_{n} \circ f_{n-1} \circ \cdots \circ f_{0}) $$ Since I need this property for a text I am writing, I would like to provide a reference. My question is the following:

Where is this result rigorously stated, and where is it rigorously proved? Hopefully, the two references will be the same.

Edit: I am aware that this result is "obvious". In addition, it is certainly classical, by which I mean that all the people working with lax functors use it routinely. However, if one wants to state it and prove it, the question arises as to what is the best way to state the result, which I think turns out not to be completely trivial. Furthermore, writing a rigorous proof certainly does require some work. I am sure there are some people here who have already used this result. How do they state it? To which reference do they point? Or is the reader assumed to find this fact so obvious that no one ever cares to provide a proof or a reference?

Answer 1

The closest statement I know is Theorem 1.6 in Gordon-Power-Street "Coherence for tricategories." It actually deals with pseudofunctors instead of lax functors, but I believe it can easily be modified to cover lax functors. The proof is the same proof of Theorem 1.7 in Joyal-Street "Braided tensor categories."

Answer 2

For composable couple of morphisms $g\circ f$ let

$T(g, f): F(g)\circ F(f) \Rightarrow F(g\circ f)$ the canonical cell.

For a triple of composable $h\circ g\circ f$ let $T_r(h, g, f):=T(T(h, g),f)$ (A short way to write $T(hg, f)\ast T(h, g)f$)

and $T_l(h,g,f):= T(h,T(g, f))$ for the axiom of coherence $T'_3=T''_3$.

If we have composable $n$ morphisms $f_n\circ \ldots\circ f_1$ for the various (associativity) coherent disposition of parenthesis (as in a no necessarily associative binary composition) we have a cell $F(f_n)\circ \ldots F(f_1) \to F(f_n\circ \ldots f_1)$, we want to prove that all these cells are equal, for $n=3$ this is true. For induction we suppose the assert for 3, ..., n and indicate with $T^k$ ($3\leq n\leq n$) the unique composition cell $F(f_k)\circ \ldots F(f_1) \to F(f_k\circ \ldots f_1)$. Let $T_{n+1}: F(f_{n+1})\circ \ldots F(f_1)\xrightarrow{1\circ T^n} F(f_{n+1})\circ F(f_n\circ \ldots f_1)\xrightarrow{T} F(f_{n+1}\circ f_n\circ \ldots f_1) $, let $T': F(f_{n+1})\circ \ldots F(f_1)\to F(f_{n+1}\circ f_n\circ \ldots f_1) $ associated to some coherent parenthesis disposition. Now if $f_{n+1}$ is not inside a parenthesis (do not allow the total parenthesis on the whole string) we have that $T'(f_{n+1}, \ldots f_1): F(f_{n+1})\circ F(f_n)\circ \ldots F(f_1)\xrightarrow{1\circ T} F(f_{n+1})\circ F(f_n\circ \ldots f_1)$ and this is $T_{n+1}$, if $f_{n+1}$ is inside a parenthesis consider the maximal parenthesis containing $f_{n+1}$ and let $f_{n+1},\ldots f_{i+1}$ the part of string contained in this parenthesis, the case $i=n-1$ follow as above,

if $i< n-1$ then

$T'(f_{n+1}, \ldots f_1)= T(T^{n-i}(f_{n+1},\ldots f_i), T^{i}(f_i,\ldots f_1))=$

$T(T((f_{n+1},T^{n-i-1}(f_n, \ldots f_i)), T^{i}(f_i,\ldots f_1))=$

$T((f_{n+1},T^n(f_n, \ldots f_1))=$

$T_{n+1}(f_{n+1}\circ \ldots f_1) $.

This is only a traslation from the classical algebra theorem.