# Commit 2022-07-27 11:14 b8fb47c4

View on Github →refactor(topology/sheaves): Redefine sheaves in terms of Grothendieck topology. (#15384)
We change the "official definition" of sheaves over topological spaces from the equalizer diagram condition to the condition in terms of the Grothendieck topology on `Opens(X)`

. The benefit is that

- The
`X.Sheaf C`

category is now defeq to`(opens.grothendieck_topology X).Sheaf C`

, so that functors between categories of sheaves over sites could be specialized onto topological spaces without the abundant equivalences. - It allows sheaves over spaces to value in arbitrary categories that doesn't have all products.
The original sheaf condition is now called
`presheaf.is_sheaf_equalizer_products`

, and`presheaf.is_sheaf_iff_is_sheaf_equalizer_products`

(in`topology.sheaves.sheaf_condition.sites`

) shows that the two are equivalent.