Lemma SumStrength2' : θ_Strength2_int θ. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.Limits.Products.