proposition: Lemma signature_from_ab_strength_law1 : θ_Strength1_int θ_for_signature.
proof: Proof. red. intro X. apply nat_trans_eq_alt. intro c. cbn. assert (HypX := triangle_eq_implies_triangle_eq_nice _ _ _ _ _ _ (ab_strength_triangle _ ab_str) X). assert (Heqc := nat_trans_eq_weq (homset_property D) _ _ HypX c). cbn in Heqc. intermediate_path (# (pr1 (H X)) (id₁ c) · id₁ (pr1(pr1 H X) c)). 2: { etrans. { apply id_right. } apply (functor_id (H X)). } etrans. 2: { exact Heqc. } clear HypX Heqc. apply maponpaths. apply nat_trans_eq_pointwise. clear c. apply maponpaths. apply nat_trans_eq_alt. intro c. cbn. apply pathsinv0. etrans. { apply id_right. } apply functor_id. 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