{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {motive : HomotopicalAlgebra.CofibrantBrownFactorization f → Sort u} →
            (t : HomotopicalAlgebra.CofibrantBrownFactorization f) →
              ((toMapFactorizationData :
                    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
                      f) →
                  (s : Y ⟶ toMapFactorizationData.Z) →
                    (s_p :
                        CategoryTheory.CategoryStruct.comp s toMapFactorizationData.p =
                          CategoryTheory.CategoryStruct.id Y) →
                      (cofibration_s : HomotopicalAlgebra.Cofibration s) →
                        motive
                          { toMapFactorizationData := toMapFactorizationData, s := s, s_p := s_p,
                            cofibration_s := cofibration_s }) →
                motive t