∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
  (Δ : SimplexCategoryᵒᵖ), (AlgebraicTopology.DoldKan.Γ₂.obj P).X.obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ P.X Δ