∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] {A B X Y : C}
  (i : A ⟶ B) (p : X ⟶ Y),
  HomotopicalAlgebra.Cofibration i →
    HomotopicalAlgebra.Fibration p → HomotopicalAlgebra.WeakEquivalence p → CategoryTheory.HasLiftingProperty i p