Commit 2022-07-27 11:14 b8fb47c4

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

1. 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.
2. 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.