(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        (n : ℤ) →
          DerivedCategory.Qh.comp (DerivedCategory.homologyFunctor C n) ≅
            HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n