{C : Type u_2} →
  [inst : CategoryTheory.Category.{v, u_2} C] →
    CategoryTheory.MorphismProperty C →
      (J : Type u_1) →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] → CategoryTheory.MorphismProperty (CategoryTheory.Functor J C)