Lemma μ_3_T_μ_2_μ_2 : μ_3 = (`T ∘ μ_2 : EndC ⟦ `T • _ , `T • `T ⟧ ) · μ_2. 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.
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.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.Notation.