Lemma isaprop_is_precategory (C : precategory_data)(hs: has_homsets C) : isaprop (is_precategory C). 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.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations.