proposition: 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: 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.
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