Lemma μ_2_is_ptd_mor : ∏ c : C, (ptd_pt C T_squared) c · μ_2 c = pr1 (η T) c. Proof. intro c. unfold μ_2. unfold T_squared. unfold ptd_compose. rewrite functorial_composition_pre_post. simpl. assert (H' := Monad_law_2_from_hss c). simpl in H'. intermediate_path (pr1 (η T) c · identity _ ). - unfold eta_from_alg; simpl. repeat rewrite <- assoc. apply maponpaths. apply maponpaths. exact H'. - apply id_right. 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.