∀ {C : Type v} [inst : CategoryTheory.Category.{v, v} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v, u₁} D]
  (F : CategoryTheory.Functor C D)
  (h : CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda))), F.Final