{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y W : C} →
      {fst : W ⟶ X} →
        {snd : W ⟶ Y} →
          (lift : (s : CategoryTheory.Limits.BinaryFan X Y) → s.pt ⟶ W) →
            (∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) →
              (∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) →
                (∀ (s : CategoryTheory.Limits.BinaryFan X Y) (m : s.pt ⟶ W),
                    CategoryTheory.CategoryStruct.comp m fst = s.fst →
                      CategoryTheory.CategoryStruct.comp m snd = s.snd → m = lift s) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd)