proposition: Lemma μ_3_μ_2_T_μ_2 : ( @compose (functor_category C C) T²∙T _ _ ((μ_2 •• `T) ) μ_2 : T•T² --> `T) = μ_3.
proof: Proof. apply (fbracket_unique T μ_2_ptd). split. - apply nat_trans_eq_alt; intro c. simpl. intermediate_path (identity _ · μ_2 c). + apply pathsinv0, id_left. + etrans; [ | apply assoc' ]. apply cancel_postcomposition. assert (H1 := Monad_law_1_from_hss (pr1 (`T) c)). apply (!H1). - set (B := τ T). match goal with | [|- _ · # ?H (?f · _ ) · _ = _ ] => set (F := f : T•T² --> _ ) end. assert (H3 := functor_comp H F μ_2). unfold functor_compose in H3. etrans. { apply cancel_postcomposition. apply maponpaths. apply H3. } clear H3. apply nat_trans_eq_alt. intro c. simpl. match goal with | [ |- ?a · _ · _ = _ ] => set (Ac := a) end. simpl in Ac. simpl in *. unfold functor_compose in *. 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. rewrite (functor_id ( H (`T))) in HXX. rewrite id_right in HXX. match goal with |[HXX : ?f · ?h = _ · _ |- _ · (_ · ?x ) · ?y = _ ] => intermediate_path (pr1 (θ ((`T) ⊗ (ptd_from_alg T))) (pr1 (pr1 (pr1 T)) c)· f · h · x · y) end. * repeat rewrite assoc. do 3 apply cancel_postcomposition. unfold Ac. clear Ac. etrans; [| apply assoc ]. etrans. 2: { apply maponpaths. apply (!HXX). } clear HXX. assert (Strength_2 : ∏ α : functor_compose (functor_composite (`T) (`T))(`T) --> functor_composite (` T) (`T), pr1 (θ (`T ⊗ T_squared)) c · pr1 (# H α) c = pr1 (θ ((`T) ⊗ (ptd_from_alg T))) ((pr1 (pr1 (pr1 T))) c)· pr1 (θ (( ((`T) • (`T) : [_, _])) ⊗ (ptd_from_alg T))) c· pr1 (# H (α : functor_compose (`T) (functor_composite (`T) (` T))--> _)) c ). { intro α; assert (HA := θ_Strength2_int_implies_θ_Strength2 _ θ_strength2_int); assert (HA' := HA (`T) (ptd_from_alg T) (ptd_from_alg T) _ α); clear HA; assert (HA2 := nat_trans_eq_pointwise HA' c ); clear HA'; simpl in HA2; apply HA2. } etrans; [ apply (Strength_2 F) |]. clear Strength_2. etrans; [ apply assoc' |]. do 2 apply maponpaths. match goal with |[ |- _ = ?pr1 (# ?G ?g) _ ] => assert (X : F = g) end. { apply nat_trans_eq; try apply homset_property. intros. unfold F. simpl. unfold horcomp_data; simpl. rewrite functor_id. apply pathsinv0, id_right. } apply (maponpaths (λ T, pr1 (# H T) c)). apply X. * clear HXX. clear Ac. clear F. clear B. assert (H4 := prejoin_from_hetsubst_τ T). assert (H5 := nat_trans_eq_pointwise H4 c); clear H4. simpl in H5. { match goal with |[ H5 : _ = ?e |- ?a · ?b · _ · _ · _ = _ ] => intermediate_path (a · b · e) end. - repeat rewrite <- assoc. do 2 apply maponpaths. repeat rewrite <- assoc in H5. apply H5. - clear H5. repeat rewrite assoc. apply cancel_postcomposition. assert (HT := prejoin_from_hetsubst_τ T). assert (H6 := nat_trans_eq_pointwise HT); clear HT. unfold coproduct_nat_trans_in2_data. unfold tau_from_alg, tau2_from_alg 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.SubstitutionSystems UniMath.SubstitutionSystems.Notation