proposition: Lemma bracket_property_for_LamE_algebra_on_Lam (Z : Ptd) (f : Ptd ⟦ Z, ptd_from_alg LamE_algebra_on_Lam ⟧) : bracket_property (nat_trans_fix_snd_arg [C, C] Ptd [C, C] (θ_source LamE_S) (θ_target LamE_S) (theta LamE_S) Z) LamE_algebra_on_Lam f (fbracket_for_LamE_algebra_on_Lam Z f).
proof: Proof. assert (Hyp := pr2 (pr1 (pr2 LamHSS _ (f · bracket_property_for_LamE_algebra_on_Lam_helper)))). apply parts_from_whole in Hyp. apply whole_from_parts. split. - apply pr1 in Hyp. apply (maponpaths (λ x, x · #U (inv_from_iso bracket_property_for_LamE_algebra_on_Lam_helper))) in Hyp. rewrite <- functor_comp in Hyp. rewrite <- assoc in Hyp. rewrite iso_inv_after_iso in Hyp. rewrite id_right in Hyp. etrans; [ exact Hyp |]. clear Hyp. fold (fbracket LamHSS (f · bracket_property_for_LamE_algebra_on_Lam_helper)). unfold fbracket_for_LamE_algebra_on_Lam. match goal with |[ |- _· _ · ?h = _ ] => assert (idness : h = nat_trans_id _) end. { apply nat_trans_eq_alt. intro c. unfold functor_ptd_forget. apply id_left. } rewrite idness. clear idness. rewrite id_right. apply nat_trans_eq_alt. intro c. apply cancel_postcomposition. apply BinCoproductIn1Commutes_right_dir. apply idpath. - destruct Hyp as [_ Hyp2]. fold (fbracket LamHSS (f · bracket_property_for_LamE_algebra_on_Lam_helper)) in Hyp2. unfold fbracket_for_LamE_algebra_on_Lam. apply nat_trans_eq_alt. intro c. rewrite τ_LamE_algebra_on_Lam. etrans; [ apply cancel_postcomposition ; apply BinCoproductOfArrows_comp |]. etrans; [ apply precompWithBinCoproductArrow |]. apply pathsinv0. apply BinCoproductArrowUnique. + etrans; [ apply assoc |]. etrans. { apply cancel_postcomposition. apply BinCoproductIn1Commutes. } assert (T:= nat_trans_eq_pointwise Hyp2 c). clear Hyp2. apply pathsinv0. assumption. + clear Hyp2. etrans; [ apply assoc |]. etrans. { apply cancel_postcomposition. apply BinCoproductIn2Commutes. } unfold Lam_Flatten. Opaque fbracket. Opaque LamHSS. set (X := f · bracket_property_for_LamE_algebra_on_Lam_helper). assert (TT := compute_fbracket C CC Lam_S LamHSS(Z:=Z)). simpl in *. assert (T3 := TT X); clear TT. unfold X; unfold X in T3; clear X. do 2 rewrite id_left. Local Notation "⦃ f ⦄" := (fbracket _ f)(at level 0). set (Tη := ptd_from_alg _ ). destruct Z as [Z e]. simpl in *. set (T := Lam). assert (T3' := nat_trans_eq_pointwise T3 c). simpl in *. match goal with |[ T3' : _ = ?f |- ?a · _ = _ ] => transitivity (a · f) end. { apply maponpaths. apply T3'. } repeat rewrite assoc. etrans. 2: { do 2 apply cancel_postcomposition. do 3 apply maponpaths. apply pathsinv0, T3'. } clear T3'. apply pathsinv0. assert (T3' := nat_trans_eq_pointwise T3 (pr1 T c)). simpl in T3'. rewrite id_right in T3'. etrans. { apply cancel_postcomposition. apply maponpaths. exact T3'. } clear T3'. apply pathsinv0. destruct f as [f fptdmor]. simpl in *. repeat rewrite assoc. rewrite <- (functor_comp (pr1 T)). repeat rewrite <- assoc. etrans. 2: { apply cancel_postcomposition. apply maponpaths. apply (nat_trans_ax e). } repeat rewrite assoc. rewrite <- (functor_comp (pr1 T)). assert (X := fptdmor ((pr1 T) c)). clear T3 fptdmor. unfold functor_identity_data. simpl. apply pathsinv0. etrans. { do 2 apply cancel_postcomposition. apply maponpaths. repeat rewrite <- assoc. do 2 apply maponpaths. apply X. } clear X. assert (X := Monad_law_2_from_hss _ CC Lam_S LamHSS ((pr1 T) c)). unfold μ_0 in X. unfold μ_2 in X. etrans. { do 2 apply cancel_postcomposition. apply maponpaths. apply assoc. } rewrite (functor_comp (pr1 T)). repeat rewrite <- assoc. match goal with |[ X : ?e = _ |- _ · (?a · (?b · _)) = _ ] => assert (X' : e = a · b) end. { apply cancel_postcomposition. apply maponpaths. cbn. apply pathsinv0, BinCoproductIn1Commutes. } rewrite X' in X. clear X'. etrans. { apply maponpaths. rewrite assoc. apply cancel_postcomposition. apply X. } clear X. rewrite id_left. assert (μ_2_nat := nat_trans_ax (μ_2 C CC Lam_S LamHSS)). assert (X := μ_2_nat _ _ (f c · identity (pr1 Lam c))). unfold μ_2 in X. etrans. 2: { rewrite assoc. apply cancel_postcomposition. apply X. } clear X. rewrite functor_comp. repeat rewrite <- assoc. apply maponpaths. assert (X := third_monad_law_from_hss _ CC Lam_S LamHSS). assert (X' := nat_trans_eq_pointwise X). clear X. simpl in X'. etrans; [ apply X' |]. clear X'. apply cancel_postcomposition. apply id_left. 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