proposition: Lemma diag_functor_fmonoidal_nat_right : preserves_tensor_nat_right (fmonoidal_preservestensordata diag_functor_fmonoidal_data).
proof: Proof. intros x1 x2 y f. apply pathsinv0. refine (_ @ naturality_inner_swap V f f (identity y) (identity y) @ _). - apply maponpaths. etrans. 2: { apply maponpaths. apply pathsinv0, (when_bifunctor_becomes_rightwhiskering V). } cbn ; apply maponpaths_2. apply pathsinv0, (when_bifunctor_becomes_rightwhiskering V). - rewrite <- (when_bifunctor_becomes_rightwhiskering V). apply maponpaths_2. apply maponpaths. apply tensor_id_id. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal