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