Lemma diag_functor_fmonoidal_assoc : preserves_associativity (fmonoidal_preservestensordata diag_functor_fmonoidal_data). Proof. intros x y z. refine (_ @ inner_swap_hexagon'_3 V x y z @ _). - now rewrite <- (when_bifunctor_becomes_rightwhiskering V). - now rewrite <- (when_bifunctor_becomes_leftwhiskering V). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Import BifunctorNotations. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal. Import MonoidalNotations.