fact: Definition model_category (C : category) := ∑ (W K F : morphism_class C), is_model_category W K F.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.ModelCategories.Lifting UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.WFS UniMath.ModelCategories.WeakEquivalences