∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {X_1 Y_1 : CategoryTheory.Limits.BinaryBicone X Y} (f : X_1 ⟶ Y_1),
  (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.map f).hom = f.hom