∀ {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.Quotient.lift r F H =
    { obj := fun a => F.obj a.as, map := fun {X Y} hf => Quot.liftOn hf (fun f => F.map f) ⋯, map_id := ⋯,
      map_comp := ⋯ }