∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {F : CategoryTheory.Functor C (Type u_1)}
  (x x_1 : CategoryTheory.Subfunctor F) (x_2 : C), x.obj x_2 ≤ { obj := fun U => x.obj U ⊔ x_1.obj U, map := ⋯ }.obj x_2