∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((SimplicialObject.Split.nondegComplexFunctor.comp (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ))).map
        Φ)
      ((fun S => S.s.toKaroubiNondegComplexIsoN₁) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun S => S.s.toKaroubiNondegComplexIsoN₁) X).hom
      (((SimplicialObject.Split.forget C).comp AlgebraicTopology.DoldKan.N₁).map Φ)