∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (hd : CategoryTheory.Limits.IsColimit d) {K₁ K₂ : CategoryTheory.Limits.Multicofork I} (f : K₁ ⟶ K₂)
  (j : CategoryTheory.Limits.WalkingParallelPair),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Multicofork.toSigmaCofork hc hd K₁).ι.app j) f.hom =
    (CategoryTheory.Limits.Multicofork.toSigmaCofork hc hd K₂).ι.app j