∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C],
  (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) →
    (∀ {d : D} {c : C} (s s' : F.obj c ⟶ d),
        ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s') →
      ∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)