∀ {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 : X ⟶ T) (g : Y ⟶ T),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inl b.toCocone)
      ((fun {T} f g => CategoryTheory.CategoryStruct.comp b.fst f + CategoryTheory.CategoryStruct.comp b.snd g) f g) =
    f