[GOAL]
J : Type v
inst✝ : Category.{v', v} J
F : J ⥤ Discrete PUnit
c s : Cone F
⊢ s.pt = c.pt
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : Category.{v', v} J
F : J ⥤ Discrete PUnit
c s : Cocone F
⊢ c.pt = s.pt
[PROOFSTEP]
simp
