∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  (H : Type u_2) [inst_1 : CategoryTheory.Category.{u_1, u_2} H]
  [inst_2 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H]
  {X Y : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} (α : X ⟶ Y) (c₁ c₂ : C) (f : c₁ ⟶ c₂),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.fiberwiseColimit X).map f)
      (CategoryTheory.Limits.colim.map ((CategoryTheory.Grothendieck.ι F c₂).whiskerLeft α)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colim.map ((CategoryTheory.Grothendieck.ι F c₁).whiskerLeft α))
      ((CategoryTheory.Limits.fiberwiseColimit Y).map f)