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. 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.
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.