∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A] [CategoryTheory.IsIso (CategoryTheory.Limits.diag A)],
  CategoryTheory.IsSubterminal A