Definition is_ptd_mor {F G : ptd_obj}(α: F ⟹ G) : UU := ∏ c : C, ptd_pt F c · α c = ptd_pt G c.
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.