∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X Y : C) {T : C} (f : T ⟶ X)
  (g : T ⟶ Y),
  CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' (ℬ X Y).isLimit f g))
      (CategoryTheory.Limits.BinaryFan.snd (ℬ X Y).cone) =
    g