∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (b : CategoryTheory.Limits.BinaryBicone X Y) {T : C} (f : T ⟶ X) (g : T ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((fun {T} f g => CategoryTheory.CategoryStruct.comp f b.inl + CategoryTheory.CategoryStruct.comp g b.inr) f g)
      (CategoryTheory.Limits.BinaryFan.fst b.toCone) =
    f