∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  (homRel : HomRel C) [inst_1 : CategoryTheory.HomRel.IsStableUnderPrecomp homRel]
  [inst_2 : CategoryTheory.HomRel.IsStableUnderPostcomp homRel] [inst_3 : W.HasQuotient homRel] {X Y : C} (f : X ⟶ Y),
  W.quotient homRel ((CategoryTheory.Quotient.functor homRel).map f) ↔ W f