Lemma free_ptd_alg_is_functor : is_functor free_ptd_alg_functor_data. Proof. split. - intros A. apply ptd_alg_mor_eq. apply pathsinv0, colim_endo_is_identity. intros i. refine (free_ptd_alg_mor_restricts _ _ @ _). rewrite functor_id. apply id_left. - red. intros X Y Z f g. apply pathsinv0, ptd_alg_mor_eq; simpl. apply colimArrowUnique; simpl. intros i. rewrite assoc. rw_left_comp (free_ptd_alg_mor_restricts f i). rewrite <- assoc. rw_right_comp (free_ptd_alg_mor_restricts g i). rewrite assoc. apply cancel_postcomposition. apply pathsinv0, functor_comp. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.