fact: Definition is_weak_equivalences {C : category} (W : morphism_class C) : UU := weq_comp_ax W × weq_cancel_left_ax W × weq_cancel_right_ax W.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.ModelCategories.MorphismClass