proposition: Lemma lunitor_preserves_leftwhiskering_with_unit : lu^{M}_{I_{ M} ⊗_{M} I_{M}} = I_{M} ⊗^{ M}_{l} lu^{M}_{I_{ M}}.
proof: Proof. apply pathsinv0. set (lun := monoidal_leftunitornat M _ _ (lu_{M} (I_{M}))). etrans. { apply (! id_right _). } etrans. 2: { apply id_right. } etrans. { apply maponpaths. exact (! pr1 (monoidal_leftunitorisolaw M I_{ M})). } etrans. { apply assoc. } etrans. { apply maponpaths_2 ; exact lun. } etrans. { apply assoc'. } apply maponpaths. apply monoidal_leftunitorisolaw. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful UniMath.CategoryTheory.opp_precat