proposition: Lemma constant_functor_fmonoidal_laxlaws : fmonoidal_laxlaws constant_functor_fmonoidal_data.
proof: Proof. repeat split ; (intro ; intros ; rewrite id_right). - rewrite (bifunctor_leftid V). apply id_left. - rewrite (bifunctor_rightid V). apply id_left. - apply pathsinv0, (monoid_to_assoc_law V m). - apply (monoid_to_unit_left_law V m). - apply (monoid_to_unit_right_law V m). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids