proposition: Lemma pentagon_eq_nice_implies_pentagon_eq_nicer : pentagon_eq_nice -> pentagon_eq_nicer.
proof: Proof. intro Heq'. intros X Z' Z. assert (Heqinst := Heq' X Z' Z). clear Heq'. rewrite Heqinst. clear Heqinst. etrans. 2: { apply id2_right. } rewrite <- vassocr. apply maponpaths. apply pathsinv0. 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)). cbn. rewrite <- vassocr. apply (lhs_left_invert_cell _ _ _ (is_invertible_2cell_lassociator _ _ _)). rewrite id2_right. rewrite vassocr. etrans. 2: { apply id2_left. } apply maponpaths_2. rewrite rwhisker_vcomp. etrans. { apply maponpaths. apply (z_iso_inv_after_z_iso (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