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