∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasCoproduct f] [inst_3 : CategoryTheory.Limits.HasCoproduct fun b => G.obj (f b)]
  (P : C) (g : (j : β) → f j ⟶ P),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaComparison G f)
      (G.map (CategoryTheory.Limits.Sigma.desc g)) =
    CategoryTheory.Limits.Sigma.desc fun j => G.map (g j)