proposition: Lemma relative_strength_from_actionbased_strength_laws : rel_strength_pentagon_eq F θ' × rel_strength_rectangle_eq F θ'.
proof: Proof. split. - red. cbn. intro v. assert (Hyp := ab_strength_triangle _ _ _ ab_str v). cbn in Hyp. fold timesV in Hyp. etrans. 2: exact Hyp. clear Hyp. rewrite <- assoc. apply maponpaths. apply pathsinv0. apply functor_comp. - red. cbn. intros w w' v. assert (Hyp := actionbased_strength_pentagon_eq_variant1variant2 _ _ _ _ ab_str (actionbased_strength_pentagon_eq_tovariant1 _ _ _ _ ab_str (ab_strength_pentagon _ _ _ ab_str)) v w' w). cbn in Hyp. unfold is_z_isomorphism_mor, pre_whisker_on_nat_z_iso in Hyp. cbn in Hyp. unfold is_z_isomorphism_mor. rewrite functor_id in Hyp. rewrite functor_comp in Hyp. rewrite assoc in Hyp. exact Hyp. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal UniMath.Bicategories.MonoidalCategories.Actions UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfCats