{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      (toPrecoverage : CategoryTheory.Precoverage C) →
        (∀ ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f],
            CategoryTheory.Presieve.singleton f ∈ toPrecoverage.coverings X) →
          (∀ ⦃X Y : C⦄ (f : Y ⟶ X),
              ∀ S ∈ toPrecoverage.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ toPrecoverage.coverings Y) →
            (∀ ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y),
                S ∈ toPrecoverage.coverings X →
                  (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ toPrecoverage.coverings Y) →
                    S.bind Ti ∈ toPrecoverage.coverings X) →
              CategoryTheory.Pretopology C