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