∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y}
  (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W),
  ↑(CategoryTheory.Limits.BinaryCofan.IsColimit.desc' h f g) = h.desc (CategoryTheory.Limits.BinaryCofan.mk f g)