{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (h : W ⟶ X) →
            (k : W ⟶ Y) →
              (H₁ : CategoryTheory.Limits.IsTerminal Z) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k ⋯) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk h k)