Lemma SumStrength2' : θ_Strength2_int θ. Proof. clear S11 S12 S21 S22 S11' S21'; intros X Z Z'. apply nat_trans_eq_alt; intro x; simpl; rewrite id_left. etrans; [ apply BinCoproductOfArrows_comp |]. apply pathsinv0. etrans; [ apply BinCoproductOfArrows_comp |]. apply pathsinv0. apply maponpaths_12. - assert (Ha:=S12' X Z Z'). simpl in Ha. assert (Ha_x := nat_trans_eq_pointwise Ha x). simpl in Ha_x. rewrite id_left in Ha_x. apply Ha_x. - assert (Ha:=S22' X Z Z'). simpl in Ha. assert (Ha_x := nat_trans_eq_pointwise Ha x). simpl in Ha_x. rewrite id_left in Ha_x. apply Ha_x. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. 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.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.Limits.BinProducts.