proposition: Lemma lax_monoidal_functors_Hstandard {F : C ⟶ D} (Fm Fm' : fmonoidal_lax M N F) : is_mon_nat_trans Fm Fm' (nat_trans_id (pr1 F)) → is_mon_nat_trans Fm' Fm (nat_trans_id (pr1 F)) → Fm = Fm'.
proof: Proof. intros H H'. apply fmonoidal_lax_eq. apply dirprodeq. - destruct H as [H _]. apply funextsec; intro c. apply funextsec; intro c'. assert (aux := H c c'). cbn in aux. rewrite id_right in aux. rewrite (bifunctor_distributes_over_id) in aux. + rewrite id_left in aux. exact aux. + apply (bifunctor_leftid N). + apply (bifunctor_rightid N). - destruct H as [_ H]. red in H. cbn in H. rewrite id_right in H. exact H. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Monads.Comonads