proposition: Lemma bracket_for_LamE_algebra_on_Lam_unique (Z : Ptd) (f : Ptd ⟦ Z, ptd_from_alg LamE_algebra_on_Lam ⟧) : ∏ t : ∑ h, bracket_property (nat_trans_fix_snd_arg _ _ _ _ _ (theta LamE_S) Z) _ f h, t = tpair (λ h, 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: Proof. intro t. apply subtypePath. - intro; apply (isaset_nat_trans (homset_property C)). - destruct t as [t Ht]; cbn. 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). cbn. rewrite id_right. etrans; [ apply HT |]. cbn. repeat rewrite assoc. apply cancel_postcomposition. apply BinCoproductIn1Commutes. + apply parts_from_whole in Ht. destruct Ht as [_ H2]. assert (H2better: nat_trans_fix_snd_arg [C, C] Ptd [C, C] (θ_source LamE_S) (θ_target LamE_S) (theta LamE_S) Z `LamE_algebra_on_Lam · # LamE_S t · BinCoproductArrow (CPEndC _ _ ) Lam_App_Abs Lam_Flatten = BinCoproductArrow (CPEndC _ _ ) Lam_App_Abs Lam_Flatten •• U Z · t). { rewrite <- τ_LamE_algebra_on_Lam. exact H2. } clear H2. apply nat_trans_eq_alt. intro c. assert (HT := nat_trans_eq_pointwise H2better c). match goal with |[_ : ?e = ?f |- _ ] => assert (X: BinCoproductIn1 _ · e = BinCoproductIn1 _ · f) end. { apply maponpaths . assumption. } clear HT. clear H2better. match goal with |[X : _ = ?f |- _ ] => transitivity f end. 2: { etrans; [apply assoc |]. apply cancel_postcomposition. apply BinCoproductIn1Commutes. } match goal with |[_ : ?e = _ |- _ ] => transitivity e end. 2: apply X. clear X. 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.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.BinSumOfSignatures UniMath.SubstitutionSystems.SubstitutionSystems UniMath.SubstitutionSystems.LamSignature UniMath.SubstitutionSystems.LiftingInitial UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems UniMath.SubstitutionSystems.Notation