proposition: Lemma third_monad_law_from_hss : (`T ∘ μ_2 : EndC ⟦ functor_composite (functor_composite `T `T) `T , `T • `T ⟧) · μ_2 = (rassociator_CAT _ _ _) · (μ_2 •• `T) · μ_2.
proof: Proof. intermediate_path μ_3; [apply pathsinv0, μ_3_T_μ_2_μ_2 | ]. apply pathsinv0. apply (fbracket_unique(Z:=T_squared) T μ_2). split. - apply nat_trans_eq_alt; intro c. simpl. rewrite assoc. intermediate_path (identity _ · μ_2 c). + apply pathsinv0, id_left. + apply cancel_postcomposition. rewrite id_left. assert (H1 := Monad_law_1_from_hss (pr1 (`T) c)). simpl in H1. apply (!H1). - do 2 rewrite functor_comp. do 4 rewrite assoc. unfold T_squared. apply nat_trans_eq_alt. intro c; simpl. assert (HTT := θ_strength2_int). assert (HX := HTT (`T) (ptd_from_alg T) (ptd_from_alg T)); clear HTT. assert (HX' := nat_trans_eq_pointwise HX c); clear HX. simpl in HX'. match goal with | [ H : _ = ?f |- _ · _ · ?g · ?h · ?i = _ ] => intermediate_path (f · g · h · i) end. + do 3 apply cancel_postcomposition. apply HX'. + clear HX'. rewrite id_left. rewrite id_right. assert (HX :=θ_nat_1 _ _ _ H θ _ _ μ_2). assert (HX1 := HX (ptd_from_alg T)); clear HX. simpl in HX1. assert (HXX := nat_trans_eq_pointwise HX1 c); clear HX1. simpl in HXX. unfold horcomp_data in HXX; simpl in HXX. match goal with | [ H : ?x = _ |- ?e · _ · _ · ?f · ?g = _ ] => intermediate_path (e · x · f · g) end. * do 2 apply cancel_postcomposition. repeat rewrite <- assoc. apply maponpaths. { match goal with | [ H : _ = ?x |- _ ] => intermediate_path x end. - clear HXX. apply maponpaths. match goal with | [ |- _ ?a ?x = _ ?b ?y ] => assert (TTT : a = b) end. { match goal with | [ |- _ ?a = _ ?b ] => assert (TTTT : a = b) end. { apply nat_trans_eq_alt. intros. simpl. unfold horcomp_data; simpl. rewrite functor_id. apply pathsinv0, id_right. } apply maponpaths. apply TTTT. } apply (nat_trans_eq_pointwise TTT). - repeat rewrite assoc. repeat rewrite assoc in HXX. apply (!HXX). } * clear HXX. assert (H4 := prejoin_from_hetsubst_τ T). assert (H5 := nat_trans_eq_pointwise H4 c); clear H4. unfold μ_2. repeat rewrite <- assoc. simpl in H5; repeat rewrite <- assoc in H5. etrans. { do 3 apply maponpaths. apply H5. } clear H5. rewrite functor_id. rewrite id_left. repeat rewrite assoc. apply cancel_postcomposition. assert (H4' := prejoin_from_hetsubst_τ T). assert (H6 := nat_trans_eq_pointwise H4' (pr1 `T c)); clear H4'. simpl in H6. unfold coproduct_nat_trans_in2_data in H6. simpl in H6. rewrite assoc in H6. apply H6. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems UniMath.SubstitutionSystems.Notation