{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F' : CategoryTheory.Functor C (Type w)} →
      (f : F' ⟶ F) → {G : CategoryTheory.Subfunctor F} → CategoryTheory.Subfunctor.range f ≤ G → (F' ⟶ G.toFunctor)