Commit 2022-11-09 03:23 85d6221d

refactor(topology/sheaf_condition): remove redundant constructions (#17378) The constructions used to prove is_sheaf_iff_is_sheaf_equalizer_products in sites.lean is redundant because the equivalence can now be achieved via is_sheaf (site version) ↔ opens_le_cover ↔ pairwise_intersections ↔ equalizer_products. Refactoring the proof of this equivalence after removal of these constructions, however, requires rearranging the import chain and moving things around, explaining the large diff. The author @justus-springer of the constructions has previously approved the removal in #11706. The universe levels in equalizer_products.lean are also fixed and generalized (a cover of a space should be indexed by a type in the same universe), leading to the addition of a few universe ascriptions.

• depends on: #17361