{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      {motive : W₁.HasFactorization W₂ → Sort u} →
        (t : W₁.HasFactorization W₂) →
          ((nonempty_mapFactorizationData : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (W₁.MapFactorizationData W₂ f)) →
              motive ⋯) →
            motive t