Lemma τ_part_of_alg_mor (T T' : @algebra_ob [C, C] Id_H) (β : @algebra_mor [C, C] Id_H T T'): #H β · τ T' = compose (C:=EndC) (τ T) β. Proof. assert (β_is_alg_mor := pr2 β). simpl in β_is_alg_mor. assert (β_is_alg_mor_inst := maponpaths (fun m:EndC⟦_,_⟧ => (BinCoproductIn2 (CPEndC _ _))· m) β_is_alg_mor); clear β_is_alg_mor. simpl in β_is_alg_mor_inst. apply nat_trans_eq_alt. intro c. assert (β_is_alg_mor_inst':= nat_trans_eq_pointwise β_is_alg_mor_inst c); clear β_is_alg_mor_inst. simpl in β_is_alg_mor_inst'. rewrite assoc in β_is_alg_mor_inst'. eapply pathscomp0. 2: { eapply pathsinv0. exact β_is_alg_mor_inst'. } clear β_is_alg_mor_inst'. apply BinCoproductIn2Commutes_right_in_ctx_dir. simpl. rewrite <- assoc. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. 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.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.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.Notation.