∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {ι : Type u_4} {S : C} {X : ι → C}
  {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type u_3} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)},
  (∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p) →
    ∀ {β : ι' → ι} {p'' : (j : ι') → X' j ⟶ X (β j)},
      (∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p'' j) (f (β j)) = CategoryTheory.CategoryStruct.comp (f' j) p) →
        ∀ (j : ι'),
          CategoryTheory.CategoryStruct.comp (p'' j) (f (β j)) = CategoryTheory.CategoryStruct.comp (p' j) (f (α j))