∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {n : ℕ} {Z Z' : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z)
  (h : Z ⟶ Z'), CategoryTheory.CategoryStruct.comp f.φ h = (f.postComp h).φ