∀ {C : Type u_2} [inst : CategoryTheory.Category.{v, u_2} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (x x_1 : CategoryTheory.Functor J C) (f : x ⟶ x_1),
  W.functorCategory J f = ∀ (j : J), W (f.app j)