∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u_5} [inst_2 : CategoryTheory.Category.{u_4, u_5} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] (X : CategoryTheory.Limits.Bicone F),
  { hom := G.map (CategoryTheory.CategoryStruct.id X).hom, wπ := ⋯, wι := ⋯ } =
    CategoryTheory.CategoryStruct.id
      { pt := G.obj X.pt, π := fun j => G.map (X.π j), ι := fun j => G.map (X.ι j), ι_π := ⋯ }