I found a very explicit counterexample by running some numbers in Rust: - Take $\mathbb C := (0 \rightarrow 1)$ the walking arrow, so that $\mathbb C^{\textsf{op}} \times \mathbb C$ becomes a commutative square of arrows $A\,;B = C\,;D$ (we take $A,B$ to always be on the top sides of the hexagon and $C,D$ to be on the bottom sides). - Take $\mathbb D := \{\{0,1\}\}$ the subcategory of $\textsf{Set}$ consisting of just the set $\{0,1\}$. Then consider the following situation, where $\textsf K_0 : \{0,1\} \rightarrow \{0,1\}$ indicates the constant map in $0$: - Take $F = G : \mathbb C^{\textsf{op}} \times \mathbb C \rightarrow \mathbb D$ doing the only possible thing on objects and mapping $A,B,C,D \mapsto \textsf K_0$. Functoriality is satisfied since $\textsf{K}_0\,;\textsf{K}_0 = \textsf{K}_0\,;\textsf{K}_0$. - Take $H : \mathbb C^{\textsf{op}} \times \mathbb C \rightarrow \mathbb D$ maps $A,B,C \mapsto \textsf K_0$ and $D \mapsto\textsf{id}$. Functoriality is satisfied since $\textsf{K}_0\,;\textsf{K}_0 = \textsf{K}_0\,;\textsf{id}$. Consider the following hexagons, where $\alpha_{i\in\{0,1\}} = \textsf{swap}$ and $\beta_{i\in\{0,1\}} := \textsf{id}$: [![Pasting of two dinaturality hexagons such their composition is not dinatural.][1]][1] Clearly the hexagons commute since the $\textsf K_0$s collapse everything together; but now the top side of the outer hexagon is $\textsf K_0$, and the bottom side is $\textsf K_1$. [Here][2] is the Rust code I used to generate this counterexample! [1]: https://i.sstatic.net/fzu18hm6.png [2]: https://github.com/iwilare/dinaturality-bruteforce