proposition: Lemma isaprop_has_homsets (C : precategory_ob_mor) : isaprop (has_homsets C).
proof: Proof. do 2 (apply impred; intro). apply isapropisaset. Qed.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations