proposition: Lemma θ_for_ab_strength_law1 : actionbased_strength_triangle_eq Mon_endo' domain_action target_action sig θ_for_ab_strength.
proof: Proof. red. intro X. assert (HypX := Sig_strength_law1 sig X). apply nat_trans_eq_alt. intro c. cbn. etrans. 2: { apply pathsinv0. etrans. { apply id_right. } etrans. { apply id_right. } apply (functor_id (sig X)). } assert (Heqc := nat_trans_eq_weq (homset_property D) _ _ HypX c). clear HypX. cbn in Heqc. etrans. 2: { exact Heqc. } clear Heqc. apply maponpaths. apply nat_trans_eq_pointwise. clear c. apply maponpaths. apply nat_trans_eq_alt. intro c. cbn. do 2 rewrite id_right. apply functor_id. Time Qed. Lemma θ_for_ab_strength_law2 : actionbased_strength_pentagon_eq Mon_endo' domain_action target_action sig θ_for_ab_strength. Proof. intros X Z' Z. apply nat_trans_eq_alt. intro c. simpl. assert (HypX := θ_Strength2_int_implies_θ_Strength2_int_nicer _ (Sig_strength_law2 sig) X Z Z'). assert (Heqc := nat_trans_eq_weq (homset_property D) _ _ HypX c). clear HypX. cbn in Heqc. etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply id_right. } apply id_left. } etrans. { etrans. { apply maponpaths_2. apply functor_id. } apply id_left. } refine (!_). etrans. { do 2 apply maponpaths_2. etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply functor_id. } apply functor_id. } apply id_left. } refine (!_). refine (Heqc @ _). clear Heqc. etrans. { do 2 apply maponpaths_2. apply id_left. } apply maponpaths. apply nat_trans_eq_pointwise. clear c. apply maponpaths. apply nat_trans_eq_alt. intro c. cbn. rewrite id_right. rewrite id_left. apply pathsinv0. apply functor_id. Time Qed. Definition ab_strength_from_signature : ab_strength_for_functors_and_pointed_functors sig. Proof. exists θ_for_ab_strength. split. - exact θ_for_ab_strength_law1. - exact θ_for_ab_strength_law2. Defined.
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