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