Definition ptd_id (F : ptd_obj) : ptd_mor F F. Proof. exists (nat_trans_id _ ). abstract ( intro c; apply id_right) . 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.