Lemma relative_strength_from_actionbased_strength_laws : rel_strength_pentagon_eq F θ' × rel_strength_rectangle_eq F θ'. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Import MonoidalNotations. Import BifunctorNotations. Import MonoidalNotations.