proposition: Lemma category_eq (C D : category) : (C:precategory_data) = (D:precategory_data) -> C=D.
proof: Proof. intro e. apply subtypePath. intro. apply isaprop_has_homsets. apply subtypePath'. { assumption. } apply isaprop_is_precategory. apply homset_property. Defined.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations