∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {F : CategoryTheory.Functor J (Type u_2)},
  (∀ {i j k : J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
      F.map fi xi = F.map fj xj → ∃ l fli flj x, F.map fli x = xi ∧ F.map flj x = xj) →
    F.IsLocallyDirected