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. 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.
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.FunctorCategory. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Monads.Comonads.