proposition: Lemma isaprop_is_precategory (C : precategory_data)(hs: has_homsets C) : isaprop (is_precategory C).
proof: Proof. apply isofhleveltotal2. { apply isofhleveltotal2. { repeat (apply impred; intro). apply hs. } intros _. repeat (apply impred; intro); apply hs. } intros _. apply isofhleveltotal2. { repeat (apply impred; intro); apply hs. } { intros. repeat (apply impred; intro). apply hs. } Qed.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations