∀ {V : Type u₁} [inst : Quiver V] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} (α_app : (v : V) → F.obj v ≅ G.obj v)
  (α_nat :
    ∀ {X Y : V} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (F.map f.toPath) (α_app Y).hom =
        CategoryTheory.CategoryStruct.comp (α_app X).hom (G.map f.toPath))
  (X : CategoryTheory.Paths V), (CategoryTheory.Paths.liftNatIso α_app α_nat).inv.app X = (α_app X).inv