{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y W : C} →
      {inl : X ⟶ W} →
        {inr : Y ⟶ W} →
          (desc : (s : CategoryTheory.Limits.BinaryCofan X Y) → W ⟶ s.pt) →
            (∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inl (desc s) = s.inl) →
              (∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inr (desc s) = s.inr) →
                (∀ (s : CategoryTheory.Limits.BinaryCofan X Y) (m : W ⟶ s.pt),
                    CategoryTheory.CategoryStruct.comp inl m = s.inl →
                      CategoryTheory.CategoryStruct.comp inr m = s.inr → m = desc s) →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr)