Lemma SumStrength1' : θ_Strength1_int θ. Proof. clear S11 S12 S21 S22 S12' S22'; intro X. apply nat_trans_eq_alt; intro x. etrans; [ apply BinCoproductOfArrows_comp |]. apply pathsinv0, BinCoproduct_endo_is_identity. + rewrite BinCoproductOfArrowsIn1. assert (Ha := nat_trans_eq_pointwise (S11' X) x). simpl in Ha. etrans; [ | apply id_left]. apply cancel_postcomposition. apply Ha. + rewrite BinCoproductOfArrowsIn2. assert (Ha := nat_trans_eq_pointwise (S21' X) x). simpl in Ha. etrans; [ | apply id_left]. apply cancel_postcomposition. apply Ha. 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.