∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C) {X Y : C} (f : Y ⟶ X)
  {S : CategoryTheory.Sieve X}, K.Saturate X S → K.Saturate Y (CategoryTheory.Sieve.pullback f S)