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. 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.
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.