∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  CategoryTheory.Functor.equiv.functor.obj F = F.obj { as := PUnit.unit }