∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) (i j : ℕ), (ChainComplex.truncate.obj C).d i j = C.d (i + 1) (j + 1)