Lemma eq_ptd_mor_cat {F G : category_Ptd} (a b : F --> G) : a = b ≃ (a : ptd_mor F G) = b. Proof. use tpair. intro H. exact H. apply idisweq. 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.