∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {X Y : CategoryTheory.Functor J C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Limits.HasColimit X] [inst_3 : CategoryTheory.Limits.HasColimit Y],
  W.functorCategory J f → W.colimitsOfShape J (CategoryTheory.Limits.colimMap f)