Commit 2022-08-24 09:35 7362d50a

feat(topology/sheaves/sheaf_condition/opens_le_cover): generalize universe (#16214)

• Generalize universe levels in the sheaf condition opens_le_cover on topological spaces and its equivalence with the sheaf condition on sites, allowing three different universe parameters as in Top.{w}, C : Type u and category.{v} C. To be used in #15934.
• Generalize universes for the sheaf condition pairwise_intersection on topological spaces. This sheaf condition also doesn't require any assumption on the category C, and its equivalence with opens_le_cover could also have universe levels at maximal generality; however, the proof is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections breaks due to the small_category restriction on category_theory.functor.initial.is_limit_whisker_equiv, which will take more work to fix, so we do not generalize the equivalence at this time.
• Generalize universes for Top.presheaf.pushforward; pullback is not generalized because it would need has_colimits_of_size. Top.sheaf.pushforward is not yet generalized.
• Fixate the universe level of Top.presheaf to be the same as Top.sheaf.