proposition: Lemma fmonoidal_data_eq {C D : category} {M : monoidal C} {N : monoidal D} {F : functor C D} (fmd1 fmd2 : fmonoidal_data M N F) : (∏ x y : C, fmonoidal_preservestensordata fmd1 x y = fmonoidal_preservestensordata fmd2 x y) -> fmonoidal_preservesunit fmd1 = fmonoidal_preservesunit fmd2 -> fmd1 = fmd2.
proof: Proof. intros pT pU. use total2_paths_f. - do 2 (apply funextsec ; intro) ; apply pT. - rewrite transportf_const. apply pU. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric