fact: Definition weak_equivalences (C : category) : UU := ∑ (W : morphism_class C), is_weak_equivalences W.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.ModelCategories.MorphismClass