Lemma diag_functor_fmonoidal_nat_left : preserves_tensor_nat_left (fmonoidal_preservestensordata diag_functor_fmonoidal_data). Proof. intros y x1 x2 f. apply pathsinv0. refine (_ @ naturality_inner_swap V (identity y) (identity y) f f @ _). - apply maponpaths. etrans. 2: { apply maponpaths. apply pathsinv0, (when_bifunctor_becomes_leftwhiskering V). } cbn ; apply maponpaths_2. apply pathsinv0, (when_bifunctor_becomes_leftwhiskering V). - rewrite <- (when_bifunctor_becomes_leftwhiskering V). do 2 apply maponpaths_2. apply tensor_id_id. 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.