∀ {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} {ι' : Type u_3} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S) {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)},
  (∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) e.hom) →
    ∀ {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)},
      (∀ (i : ι),
          CategoryTheory.CategoryStruct.comp (q' i) (f' (β i)) = CategoryTheory.CategoryStruct.comp (f i) e.inv) →
        ∀ (k : ι'),
          CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (p' k) (q' (α k))) (f' ((β ∘ α) k)) =
            CategoryTheory.CategoryStruct.comp (f' k) (CategoryTheory.CategoryStruct.id S')