proposition: Lemma μ_3_T_μ_2_μ_2 : μ_3 = (`T ∘ μ_2 : EndC ⟦ `T • _ , `T • `T ⟧ ) · μ_2.
proof: Proof. apply pathsinv0. apply (fbracket_unique T μ_2_ptd). split. - apply nat_trans_eq_alt. intro c. assert (H2 := nat_trans_ax (η T)); simpl in H2. rewrite assoc. simpl; rewrite <- H2 ; clear H2. intermediate_path (μ_2 c · identity _ ). + apply pathsinv0, id_right. + etrans; [| apply assoc ]. apply maponpaths. apply pathsinv0. apply Monad_law_1_from_hss. - rewrite functor_comp. assert (H1 := θ_nat_2 _ _ _ H θ (`T) _ _ μ_2_ptd). simpl in H1. repeat rewrite assoc. match goal with |[H1 : ?g = _ |- _ · _ · ?f · ?h = _ ] => intermediate_path (g · f · h) end. + do 2 apply cancel_postcomposition. apply pathsinv0. etrans; [apply H1 |]. clear H1. do 2 apply maponpaths. assert (H3 := horcomp_id_postwhisker). assert (H4 := H3 _ _ _ _ _ μ_2 (`T)); clear H3. apply H4. + clear H1. apply nat_trans_eq_alt. intro c; simpl. unfold horcomp_data; simpl. rewrite id_left. assert (H2 := prejoin_from_hetsubst_τ T). assert (H3 := nat_trans_eq_pointwise H2 c); clear H2. simpl in *. match goal with |[H3 : _ = ?f |- ?e · _ · _ · _ = _ ] => intermediate_path (e · f) end. * etrans; [ apply assoc' |]. etrans; [ apply assoc' |]. apply maponpaths. etrans; [| apply H3 ]. apply assoc. * clear H3. repeat rewrite assoc. apply cancel_postcomposition. assert (H1 := nat_trans_ax (τ T )). unfold tau_from_alg in H1. etrans; [ | apply H1]; clear H1. apply assoc'. 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.SubstitutionSystems UniMath.SubstitutionSystems.Notation