∀ {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] (i j k : ℕ),
  CategoryTheory.CategoryStruct.comp (s.d i j) (s.d j k) = 0