∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} 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) (m : W ⟶ s.pt),
      CategoryTheory.CategoryStruct.comp inl m = s.inl →
        CategoryTheory.CategoryStruct.comp inr m = s.inr → m = desc s) →
    ∀ (s : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y))
      (m : (CategoryTheory.Limits.BinaryCofan.mk inl inr).pt ⟶ s.pt),
      (∀ (j : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
          CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.BinaryCofan.mk inl inr).ι.app j) m = s.ι.app j) →
        m = desc s