Lemma eq_ptd_mor {F G : ptd_obj} (a b : ptd_mor F G) : a = b ≃ (a : F ⟹ G) = b. Proof. apply subtypeInjectivity. intro x. apply impred; intro. apply homset_property. 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.