proposition: Lemma isprop_is_model_category {C : category} (W K F : morphism_class C) : isaprop (is_model_category W K F).
proof: Proof. apply isapropdirprod. apply isaprop_is_weak_equivalences. apply isapropdirprod; apply isaprop_is_wfs. Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.ModelCategories.Lifting UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.WFS UniMath.ModelCategories.WeakEquivalences