∀ {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] (F : V ⥤q W) {U : Type u₃} [inst_2 : Quiver U]
  (G : W ⥤q U) {a b : V} (p : Quiver.Path a b), (F ⋙q G).mapPath p = G.mapPath (F.mapPath p)