Lemma SumStrength2 : θ_Strength2 θ. Proof. intros X Z Z' Y α. apply nat_trans_eq_alt; intro x. etrans; [ apply BinCoproductOfArrows_comp |]. apply pathsinv0. etrans. { apply cancel_postcomposition. simpl. apply BinCoproductOfArrows_comp. } etrans; [apply BinCoproductOfArrows_comp |]. apply pathsinv0. apply maponpaths_12. - assert (Ha:=S12 X Z Z' Y α). simpl in Ha. assert (Ha_x := nat_trans_eq_pointwise Ha x). apply Ha_x. - assert (Ha:=S22 X Z Z' Y α). simpl in Ha. assert (Ha_x := nat_trans_eq_pointwise 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.