(A : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [inst_1 : CategoryTheory.Abelian A] →
      AlgebraicTopology.DoldKan.N₁ ≅
        (AlgebraicTopology.normalizedMooreComplex A).comp (CategoryTheory.Idempotents.toKaroubi (ChainComplex A ℕ))