∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] {Y : C} {S : CategoryTheory.Functor C D} [inst_2 : S.Full]
  [S.Faithful]
  (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty (CategoryTheory.CostructuredArrow S (S.obj Y))))
  (m :
    s.pt ⟶
      (CategoryTheory.Limits.asEmptyCone
          (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (S.obj Y)))).pt),
  (∀ (j : CategoryTheory.Discrete PEmpty.{1}),
      CategoryTheory.CategoryStruct.comp m
          ((CategoryTheory.Limits.asEmptyCone
                  (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (S.obj Y)))).π.app
            j) =
        s.π.app j) →
    m = CategoryTheory.CostructuredArrow.homMk (S.preimage s.pt.hom) ⋯