∀ {J : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} J} (F : CategoryTheory.Functor J (Type u_2))
  [self : F.IsLocallyDirected] {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