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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Import Bicat.Notations. Section Action_From_Precomposition. End Action_From_Precomposition.