∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C] {X : C}
  (S : CategoryTheory.Sieve X),
  S ∈ (CategoryTheory.extensiveTopology C) X ↔
    ∃ α,
      ∃ (_ : Finite α),
        ∃ Y π,
          Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)