∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂)
  (Φ : CategoryTheory.Functor (CategoryTheory.Quotient r) D),
  (CategoryTheory.Quotient.functor r).comp Φ = F → Φ = CategoryTheory.Quotient.lift r F H