proposition: Lemma SumStrength2' : θ_Strength2_int θ.
proof: Proof. intros X Z Z'. apply nat_trans_eq_alt; intro x; simpl; rewrite id_left. etrans; [apply CoproductOfArrows_comp|]. apply pathsinv0. etrans; [apply CoproductOfArrows_comp|]. apply pathsinv0, maponpaths, funextsec; intro i. assert (Ha_x := nat_trans_eq_pointwise (S12' i X Z Z') x); simpl in Ha_x. rewrite id_left in Ha_x; apply Ha_x. Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PointedFunctorsComposition UniMath.SubstitutionSystems.Signatures UniMath.CategoryTheory.Limits.Coproducts UniMath.SubstitutionSystems.Notation UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.Limits.Products