∀ {I : Type u_2} {C : I → Type u_3} [inst : (i : I) → CategoryTheory.Category.{u_1, u_3} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)]
  (X : (i : I) → C i) {X_1 Y Z : (i : I) → C i} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
  (fun i => (CategoryTheory.ihom (X i)).map (CategoryTheory.CategoryStruct.comp f g i)) =
    CategoryTheory.CategoryStruct.comp (fun i => (CategoryTheory.ihom (X i)).map (f i)) fun i =>
      (CategoryTheory.ihom (X i)).map (g i)