proposition: Lemma Monad_law_2_from_hss: ∏ c : C, # (pr1 (`T)) (μ_0 c)· μ_2 c = identity ((pr1 (`T)) c).
proof: Proof. intro c. intermediate_path (μ_1 c). - unfold μ_1. assert (H' := @fbracket_unique_target_pointwise _ _ _ T). assert (H1 := H' (id_Ptd C) μ_0). set (x := post_whisker μ_0 (`T) : EndC ⟦ `T • functor_identity _ , `T • `T ⟧). set (x' := x · μ_2). assert (H2 := H1 x'). apply H2; clear H2. unfold x'. clear x'. unfold x; clear x. clear H1. clear H'. clear c. split. + apply nat_trans_eq_alt. intro c. assert (H' := nat_trans_ax (η T)). simpl in H'. rewrite assoc. cbn. rewrite <- H'; clear H'. assert (H' := prejoin_from_hetsubst_η T). assert (H2 := nat_trans_eq_weq (homset_property C) _ _ H'). simpl in H2. rewrite <- assoc. rewrite <- H2. apply pathsinv0. apply id_right. + rewrite functor_comp. apply nat_trans_eq_alt. intro c. rewrite <- horcomp_id_postwhisker. do 2 rewrite assoc. simpl in *. unfold horcomp_data; simpl. intermediate_path ( # (pr1 (H ( (` T)))) (μ_0 c) · pr1 (θ ((`T) ⊗ (p T))) c · pr1 (# H μ_2) c · pr1 (τ T) c). * unfold tau_from_alg; cbn. do 2 rewrite assoc. do 3 apply cancel_postcomposition. assert (H' := θ_nat_2 _ _ _ H θ). assert (H2 := H' (`T) _ _ μ_0_ptd); clear H'. assert (H3 := nat_trans_eq_weq (homset_property C) _ _ H2 c); clear H2. simpl in H3. unfold horcomp_data in H3; simpl in H3. rewrite id_left in H3. apply (!H3). * assert (H' := prejoin_from_hetsubst_τ T). assert (H2 := nat_trans_eq_weq (homset_property C) _ _ H' c); clear H'. simpl in *. do 2 rewrite <- assoc. { intermediate_path ( # (pr1 (H (` T))) (μ_0 c) · (pr1 (τ T) (pr1 (`T) c) · pr1 μ_2 c)). - apply maponpaths. rewrite assoc. apply H2. - clear H2. do 2 rewrite assoc. apply cancel_postcomposition. etrans. { apply (nat_trans_ax (τ T) ). } apply cancel_postcomposition. apply pathsinv0. apply id_right. } - apply μ_1_identity'. 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.SimplifiedHSS.SubstitutionSystems UniMath.SubstitutionSystems.Notation