proposition: Lemma action_from_precomp_laws : action_triangle_eq Mon_endo homcat precomp_odot precomp_right_unitor precomp_convertor × action_pentagon_eq Mon_endo homcat precomp_odot precomp_convertor.
proof: Proof. split. - red. cbn. intros a x. rewrite hcomp_identity_right. rewrite hcomp_identity_left. apply pathsinv0. apply runitor_rwhisker. - red. cbn. intros a x y z. rewrite hcomp_identity_left. rewrite hcomp_identity_right. apply pathsinv0. apply lassociator_lassociator. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory UniMath.Bicategories.MonoidalCategories.Actions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfCats