proposition: Lemma is_functor_ptd_from_alg_functor_data : is_functor ptd_from_alg_functor_data.
proof: Proof. split; simpl; intros. + unfold functor_idax. intro T. apply (invmap (eq_ptd_mor_cat _ _ _)). apply (invmap (eq_ptd_mor _ _)). apply idpath. + unfold functor_compax. intros T T' T'' β β'. apply (invmap (eq_ptd_mor_cat _ _ _)). apply (invmap (eq_ptd_mor _ _)). 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