Lemma has_homsets_precategory_Ptd: has_homsets precategory_Ptd. 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.
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.