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. intros pT pU. use total2_paths_f. - do 2 (apply funextsec ; intro) ; apply pT. - rewrite transportf_const. apply pU. 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import BifunctorNotations. Import MonoidalNotations.