∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (i : ℕ),
  (AlgebraicTopology.DoldKan.N₂.obj P).p.f i =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f i)
      (P.p.app (Opposite.op (SimplexCategory.mk i)))