proposition: Lemma Gθ_Strength1_int : θ_Strength1_int Gθ.
proof: Proof. intro F. apply nat_trans_eq_alt; intro c; simpl. rewrite <- assoc. rewrite id_left. etrans. { apply pathsinv0, functor_comp. } apply pathsinv0; etrans. { apply pathsinv0, functor_id. } apply maponpaths. generalize (nat_trans_eq_pointwise (θ_strength1 F) c); simpl. intro Hyp. apply pathsinv0, Hyp. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.PointedFunctors UniMath.SubstitutionSystems.Signatures UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.Notation UniMath.CategoryTheory.PointedFunctorsComposition