Lemma is_ptd_mor_alg_mor (T T' : @algebra_ob [C, C] Id_H) (β : @algebra_mor [C, C] Id_H T T') : @is_ptd_mor C (ptd_from_alg T) (ptd_from_alg T') (pr1 β). Proof. simpl. unfold is_ptd_mor. simpl. intro c. rewrite <- assoc. assert (X:=pr2 β). assert (X':= nat_trans_eq_pointwise X c). simpl in *. etrans. { apply maponpaths. apply X'. } unfold coproduct_nat_trans_in1_data. repeat rewrite assoc. unfold coproduct_nat_trans_data. etrans. { apply cancel_postcomposition. apply BinCoproductIn1Commutes. } simpl. repeat rewrite <- assoc. apply id_left. 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.