{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] →
              (X : C) → CategoryTheory.Limits.IsTerminal X → Unique (CategoryTheory.ToType X)