∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y))
  (h : CategoryTheory.Limits.IsLimit b.toBinaryBicone.toCone)
  (h' : CategoryTheory.Limits.IsColimit b.toBinaryBicone.toCocone),
  (fun h =>
        { isLimit := b.toBinaryBiconeIsLimit.symm h.isLimit, isColimit := b.toBinaryBiconeIsColimit.symm h.isColimit })
      ((fun h => { isLimit := b.toBinaryBiconeIsLimit h.isLimit, isColimit := b.toBinaryBiconeIsColimit h.isColimit })
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' }