proposition: Lemma isaprop_is_weak_equivalences {C : category} (W : morphism_class C) : isaprop (is_weak_equivalences W).
proof: Proof. idtac; repeat apply isapropdirprod; do 3 (apply impred_isaprop; intro); apply propproperty. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.ModelCategories.MorphismClass