∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {W X Y Z : CategoryTheory.Limits.Bicone F}
  (f : CategoryTheory.Limits.BiconeMorphism W X) (g : CategoryTheory.Limits.BiconeMorphism X Y)
  (h : CategoryTheory.Limits.BiconeMorphism Y Z),
  {
      hom :=
        CategoryTheory.CategoryStruct.comp
          { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, wπ := ⋯, wι := ⋯ }.hom h.hom,
      wπ := ⋯, wι := ⋯ } =
    {
      hom :=
        CategoryTheory.CategoryStruct.comp f.hom
          { hom := CategoryTheory.CategoryStruct.comp g.hom h.hom, wπ := ⋯, wι := ⋯ }.hom,
      wπ := ⋯, wι := ⋯ }