∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) × C i}
  (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f