{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasInitial C] →
      [CategoryTheory.Limits.InitialMonoClass C] → {X : C} → OrderBot (CategoryTheory.Subobject X)