{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      {motive : W₁.FunctorialFactorizationData W₂ → Sort u} →
        (t : W₁.FunctorialFactorizationData W₂) →
          ((Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C) →
              (i : CategoryTheory.Arrow.leftFunc ⟶ Z) →
                (p : Z ⟶ CategoryTheory.Arrow.rightFunc) →
                  (fac : CategoryTheory.CategoryStruct.comp i p = CategoryTheory.Arrow.leftToRight) →
                    (hi : ∀ (f : CategoryTheory.Arrow C), W₁ (i.app f)) →
                      (hp : ∀ (f : CategoryTheory.Arrow C), W₂ (p.app f)) →
                        motive { Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp }) →
            motive t