∀ {I : Type u_1} {C : I → Type u_2} [inst : (i : I) → CategoryTheory.Category.{u_3, u_2} (C i)]
  (motive : (x x_1 : (i : I) × C i) → (x ⟶ x_1) → Prop) (x x_1 : (i : I) × C i) (x_2 : x ⟶ x_1),
  (∀ (i : I) (X Y : C i) (a : X ⟶ Y), motive ⟨i, X⟩ ⟨i, Y⟩ (CategoryTheory.Sigma.SigmaHom.mk a)) → motive x x_1 x_2