∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : CategoryTheory.SimplicialObject C}
  (s : SimplicialObject.Splitting X) [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.CategoryStruct.comp
      {
        f :=
          {
            f := fun n =>
              CategoryTheory.CategoryStruct.comp
                ((s.cofan (Opposite.op (SimplexCategory.mk n))).inj
                  (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n))))
                (AlgebraicTopology.DoldKan.PInfty.f n),
            comm' := ⋯ },
        comm := ⋯ }
      {
        f :=
          { f := fun n => s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n))),
            comm' := ⋯ },
        comm := ⋯ } =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)