proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.Notation