∀ {C : Type u_5} [inst : CategoryTheory.Category.{u_4, u_5} C] {α : Type u_2} {I : α → Type u_3}
  [inst_1 : (i : α) → CategoryTheory.Category.{u_1, u_3} (I i)]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (F : (i : α) → CategoryTheory.Functor (I i) C) {X Y Z : (i : α) → I i} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.Limits.Pi.map fun s => (F s).map (CategoryTheory.CategoryStruct.comp f g s)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map fun s => (F s).map (f s))
      (CategoryTheory.Limits.Pi.map fun s => (F s).map (g s))