∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {D : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_2, u_3} D] (F : CategoryTheory.Functor C D) (r : HomRel C) (A : Type u_5)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : r.IsCompatibleWithShift A] [inst_6 : F.CommShift A]
  (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂),
  CategoryTheory.Quotient.LiftCommShift.iso F r hF 0 =
    CategoryTheory.Functor.CommShift.isoZero (CategoryTheory.Quotient.lift r F hF) A