∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X : C}
  {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y),
  S ∈ (J.over X) Y ↔ (CategoryTheory.Sieve.overEquiv Y) S ∈ J Y.left