{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {V : Type u₁} →
      [inst_1 : Quiver V] →
        {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} →
          (α_app : (v : V) → F.obj v ⟶ G.obj v) →
            (∀ {X Y : V} (f : X ⟶ Y),
                CategoryTheory.CategoryStruct.comp (F.map f.toPath) (α_app Y) =
                  CategoryTheory.CategoryStruct.comp (α_app X) (G.map f.toPath)) →
              (F ⟶ G)