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 _ _ _ _ _ (theta LamE_S) Z) _ f (fbracket_for_LamE_algebra_on_Lam Z f). 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. match goal with | [ |- _ = _ · ?l ] => let ty:= (type of l) in idtac ty end. *) 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. change (pr1 ⦃ identity (ptd_from_alg (pr1 LamHSS)) ⦄ c) with (prejoin_from_hetsubst LamHSS c). 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.
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.