∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Quotient.functor r).homRel f g ↔ Relation.EqvGen (CategoryTheory.HomRel.CompClosure r) f g