Lemma bracket_for_LamE_algebra_on_Lam_unique (Z : Ptd) (f : Ptd ⟦ Z, ptd_from_alg LamE_algebra_on_Lam ⟧) : ∏ t : ∑ h : [C, C] ⟦ functor_composite (U Z) (` LamE_algebra_on_Lam), `LamE_algebra_on_Lam ⟧, bracket_property (nat_trans_fix_snd_arg _ _ _ _ _ (theta LamE_S) Z) _ f h, t = tpair (λ h : [C, C] ⟦ functor_composite (U Z) (` LamE_algebra_on_Lam), `LamE_algebra_on_Lam ⟧, bracket_property (nat_trans_fix_snd_arg _ _ _ _ _ (theta LamE_S) Z) _ f h) (fbracket_for_LamE_algebra_on_Lam Z f) (bracket_property_for_LamE_algebra_on_Lam Z f). Proof. intro t. apply subtypePath. - intro; apply (isaset_nat_trans (homset_property C)). - simpl. destruct t as [t Ht]; simpl. unfold fbracket_for_LamE_algebra_on_Lam. apply (fbracket_unique LamHSS). split. + apply parts_from_whole in Ht. destruct Ht as [H1 _]. apply nat_trans_eq_alt. intro c. assert (HT := nat_trans_eq_pointwise H1 c). simpl. rewrite id_right. etrans; [ apply HT |]. simpl. repeat rewrite assoc. apply cancel_postcomposition. apply BinCoproductIn1Commutes. + apply parts_from_whole in Ht. destruct Ht as [_ H2]. apply nat_trans_eq_alt. intro c. assert (HT := nat_trans_eq_pointwise H2 c). match goal with |[H2 : ?e = ?f |- _ ] => assert (X: BinCoproductIn1 _ · e = BinCoproductIn1 _ · f) end. { apply maponpaths . assumption. } clear HT. clear H2. match goal with |[X : _ = ?f |- _ ] => transitivity f end. 2: { rewrite τ_LamE_algebra_on_Lam. etrans; [apply assoc |]. apply cancel_postcomposition. apply BinCoproductIn1Commutes. } match goal with |[X : ?e = _ |- _ ] => transitivity e end. 2: apply X. rewrite τ_LamE_algebra_on_Lam. apply pathsinv0. etrans; [ apply assoc |]. etrans. { apply cancel_postcomposition. apply assoc. } etrans. { apply cancel_postcomposition. apply cancel_postcomposition. apply BinCoproductIn1Commutes. } repeat rewrite <- assoc. etrans. { apply maponpaths. apply assoc. } etrans. { apply maponpaths. apply cancel_postcomposition. apply BinCoproductIn1Commutes. } etrans. { apply maponpaths. apply assoc'. } simpl. do 2 apply maponpaths. apply BinCoproductIn1Commutes. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.BinSumOfSignatures. Require Import UniMath.SubstitutionSystems.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.LamSignature. Require Import UniMath.SubstitutionSystems.LiftingInitial. Require Import UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems. Require Import UniMath.SubstitutionSystems.Notation.