proposition: Lemma action_pentagon_eq_from_alt: action_pentagon_eq odot χ.
proof: Proof. intros a x y z. cbn. rewrite functor_id. do 5 rewrite id_left. do 4 rewrite id_right. assert (aux := functor_id FF z). apply (maponpaths pr1) in aux. apply toforallpaths in aux. rewrite aux. cbn. rewrite id_right. assert (Hassoc := FFassoc x y z). apply (maponpaths pr1) in Hassoc. apply toforallpaths in Hassoc. assert (Hassocinst := Hassoc a). clear Hassoc. cbn in Hassocinst. rewrite id_right, id_left in Hassocinst. do 2 rewrite functor_id in Hassocinst. rewrite id_left in Hassocinst. apply pathsinv0. exact Hassocinst. Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal