Definition ptd_forget_data : functor_data category_Ptd [C, C]. Proof. exists (λ a, pr1 a). exact (λ a b f, pr1 f). Defined.
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.