{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (categoryWithFibrations :
        autoParam (HomotopicalAlgebra.CategoryWithFibrations C)
          HomotopicalAlgebra.ModelCategory.categoryWithFibrations._autoParam) →
      (categoryWithCofibrations :
          autoParam (HomotopicalAlgebra.CategoryWithCofibrations C)
            HomotopicalAlgebra.ModelCategory.categoryWithCofibrations._autoParam) →
        (categoryWithWeakEquivalences :
            autoParam (HomotopicalAlgebra.CategoryWithWeakEquivalences C)
              HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences._autoParam) →
          autoParam (CategoryTheory.Limits.HasFiniteLimits C) HomotopicalAlgebra.ModelCategory.cm1a._autoParam →
            autoParam (CategoryTheory.Limits.HasFiniteColimits C) HomotopicalAlgebra.ModelCategory.cm1b._autoParam →
              autoParam (HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty
                  HomotopicalAlgebra.ModelCategory.cm2._autoParam →
                autoParam (HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts
                    HomotopicalAlgebra.ModelCategory.cm3a._autoParam →
                  autoParam (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts
                      HomotopicalAlgebra.ModelCategory.cm3b._autoParam →
                    autoParam (HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts
                        HomotopicalAlgebra.ModelCategory.cm3c._autoParam →
                      autoParam
                          (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i]
                            [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p],
                            CategoryTheory.HasLiftingProperty i p)
                          HomotopicalAlgebra.ModelCategory.cm4a._autoParam →
                        autoParam
                            (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i]
                              [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence p],
                              CategoryTheory.HasLiftingProperty i p)
                            HomotopicalAlgebra.ModelCategory.cm4b._autoParam →
                          autoParam
                              ((HomotopicalAlgebra.trivialCofibrations C).HasFactorization
                                (HomotopicalAlgebra.fibrations C))
                              HomotopicalAlgebra.ModelCategory.cm5a._autoParam →
                            autoParam
                                ((HomotopicalAlgebra.cofibrations C).HasFactorization
                                  (HomotopicalAlgebra.trivialFibrations C))
                                HomotopicalAlgebra.ModelCategory.cm5b._autoParam →
                              HomotopicalAlgebra.ModelCategory C