∀ {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₁ F₂ : CategoryTheory.Functor (CategoryTheory.Quotient r) D),
  (CategoryTheory.Quotient.functor r).comp F₁ = (CategoryTheory.Quotient.functor r).comp F₂ → F₁ = F₂