Lemma is_functor_ptd_from_alg_functor_data : is_functor ptd_from_alg_functor_data. 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.
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.