∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{w, v, u} Q], P ≤ Q → CategoryTheory.ObjectProperty.Small.{w, v, u} P