fact: Definition make_is_model_category {C : category} (W K F : morphism_class C) (weq : is_weak_equivalences W) (cfw_wfs : is_wfs K (F ∩ W)) (cwf_wfs : is_wfs (K ∩ W) F) : is_model_category W K F := make_dirprod weq (make_dirprod cfw_wfs cwf_wfs).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.ModelCategories.Lifting UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.WFS UniMath.ModelCategories.WeakEquivalences