{T : Type u} →
  [inst : CategoryTheory.Category.{u, u} T] →
    CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of T) →
      (CategoryTheory.Cat.of T ≅ CategoryTheory.Cat.of (CategoryTheory.Discrete PUnit.{u + 1}))