Lemma Monad_law_2_from_hss: ∏ c : C, # (pr1 (`T)) (μ_0 c)· μ_2 c = identity ((pr1 (`T)) c). Proof. intro c. intermediate_path (μ_1 c). - unfold μ_1. assert (H' := @fbracket_unique_target_pointwise _ _ _ T). assert (H1 := H' _ μ_0_ptd). 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.
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.