∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {X Y : ChainComplex C ℕ} (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ),
  (AlgebraicTopology.DoldKan.Γ₀.map f).app Δ =
    (AlgebraicTopology.DoldKan.Γ₀.splitting X).desc Δ fun A =>
      CategoryTheory.CategoryStruct.comp (f.f (Opposite.unop A.fst).len)
        (((AlgebraicTopology.DoldKan.Γ₀.splitting Y).cofan Δ).inj A)