∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q q_1 : ℕ),
  q = q_1 →
    ∀ (n m : ℕ) (a : AlgebraicTopology.DoldKan.c.Rel m n),
      AlgebraicTopology.DoldKan.hσ' q n m a = AlgebraicTopology.DoldKan.hσ' q_1 n m a