∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} (Z : C) (i : X ⟶ Z) (p : Z ⟶ Y)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp i p = f)
      CategoryTheory.MorphismProperty.MapFactorizationData.fac._autoParam)
  (hi : W₁ i) (hp : W₂ p) (Z_1 : C) (i_1 : X ⟶ Z_1) (p_1 : Z_1 ⟶ Y)
  (fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i_1 p_1 = f)
      CategoryTheory.MorphismProperty.MapFactorizationData.fac._autoParam)
  (hi_1 : W₁ i_1) (hp_1 : W₂ p_1),
  ({ Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp } =
      { Z := Z_1, i := i_1, p := p_1, fac := fac_1, hi := hi_1, hp := hp_1 }) =
    (Z = Z_1 ∧ i ≍ i_1 ∧ p ≍ p_1)