∀ {I : Type u_5} {C : I → Type u_2} [inst : (i : I) → CategoryTheory.Category.{u_1, u_2} (C i)] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (i : I) {X Y : C i}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.Sigma.incl i).comp (CategoryTheory.Sigma.desc F)).map f)
      ((fun x => CategoryTheory.Iso.refl (((CategoryTheory.Sigma.incl i).comp (CategoryTheory.Sigma.desc F)).obj x))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x => CategoryTheory.Iso.refl (((CategoryTheory.Sigma.incl i).comp (CategoryTheory.Sigma.desc F)).obj x))
          X).hom
      ((F i).map f)