Lemma μ_3_μ_2_T_μ_2 : ( @compose (functor_category C C) T²∙T _ _ ((μ_2 •• `T) ) μ_2 : T•T² --> `T) = μ_3. Proof. apply (fbracket_unique(Z:=T_squared) T μ_2). 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.Notation.