∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C] {X : C}
  (S : CategoryTheory.Sieve X),
  S ∈ (CategoryTheory.coherentTopology C) X ↔
    ∃ α, ∃ (_ : Finite α), ∃ Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)