Lemma action_pentagon_eq_from_alt: action_pentagon_eq odot χ. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. 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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal.