Lemma strength_law2_pw : ∏ (X : EndC) (Z Z' : Ptd) x, ((theta H) (X ⊗ (Z p• Z')) : nat_trans _ _) x = ((theta H) (X ⊗ Z') •• (U Z):nat_trans _ _) x · ((theta H) ((functor_compose (U Z') X) ⊗ Z):nat_trans _ _) x · (# H (identity (functor_compose (U Z ∙ U Z') X) : [C, C] ⟦ functor_compose (U Z) (U Z' ∙ X : [C, C]), functor_compose (U Z ∙ U Z') X ⟧) : nat_trans _ _) x. Proof. intros X Z Z' x. etrans; revgoals. { apply (nat_trans_eq_pointwise (θ_Strength2_int_implies_θ_Strength2 _ (Sig_strength_law2 H) X Z Z' _ (identity _) ) x). } etrans;[eapply pathsinv0;apply id_right|]. apply cancel_precomposition. apply pathsinv0. etrans. { eapply nat_trans_eq_pointwise. apply (functor_id H). } apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. 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.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Monads.LModules. Require Import UniMath.SubstitutionSystems.SubstitutionSystems. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.SubstitutionSystems.LiftingInitial_alt. Require Import UniMath.SubstitutionSystems.GenMendlerIteration_alt. Require Import UniMath.CategoryTheory.Limits.Initial.