proposition: Lemma pentagon_eq_nicer_implies_pentagon_eq_nice : pentagon_eq_nicer -> pentagon_eq_nice.
proof: Proof. intro Heq. intros X Z' Z. specialize (Heq X Z' Z). etrans. 2: { apply maponpaths_2. exact Heq. } clear Heq. repeat rewrite <- vassocr. do 2 apply maponpaths. etrans. { apply pathsinv0. apply id2_right. } apply maponpaths. etrans. 2: { apply (functor_comp(C:=hom c0 d0')(C':=hom c0 d0)). } apply pathsinv0. apply (functor_id_id (hom c0 d0') (hom c0 d0)). refine (vassocr _ _ _ @ _). etrans. { apply maponpaths_2. apply vassocl. } etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply rassociator_lassociator. } apply id2_right. } rewrite rwhisker_vcomp. etrans. { apply maponpaths. apply (z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso (strong_monoidal_functor_μ U) (Z',,Z))). } apply id2_rwhisker. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.Bicategories.MonoidalCategories.PointedFunctorsMonoidal UniMath.Bicategories.MonoidalCategories.Actions UniMath.Bicategories.MonoidalCategories.ConstructionOfActions UniMath.Bicategories.MonoidalCategories.ActionOfEndomorphismsInBicat UniMath.Bicategories.MonoidalCategories.ActionBasedStrength UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorCategory UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.SignatureCategory UniMath.CategoryTheory.Core.Univalence