∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{1}) C) (Y : C) (u : (X : C) → Unique (X ⟶ Y))
  (s : CategoryTheory.Limits.Cone F) (j : CategoryTheory.Discrete PEmpty.{1}),
  CategoryTheory.CategoryStruct.comp default
      ({ pt := Y,
              π := { app := fun X => id (CategoryTheory.Discrete.casesOn X fun as => ⋯.elim), naturality := ⋯ } }.π.app
        j) =
    s.π.app j