{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} →
        CategoryTheory.Limits.IsLimit s →
          {t : CategoryTheory.Limits.BinaryFan X s.pt} → CategoryTheory.Limits.IsLimit t → (t.pt ≅ X)