proposition: Lemma has_homsets_precategory_Ptd: has_homsets precategory_Ptd.
proof: Proof. red. intros F G. red. intros a b. apply (isofhlevelweqb 1 (eq_ptd_mor a b)). apply (homset_property (functor_category C C)). Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory