proposition: Lemma is_mon_nat_trans_identity {C D : category} {M : monoidal C} {N : monoidal D} {F : functor C D} (Fm : fmonoidal_lax M N F) : is_mon_nat_trans Fm Fm (nat_trans_id _).
proof: Proof. split; red; cbn; unfold fmonoidal_preservestensordata, fmonoidal_preservesunit; intros. - etrans. 2: { apply cancel_postcomposition. apply pathsinv0, bifunctor_distributes_over_id. - cbn in *. apply (bifunctor_leftid N). - cbn in *. apply (bifunctor_rightid N). } rewrite id_left. apply id_right. - apply id_right. 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