mathlib3

20e597fb - chore(topology/sheaf_condition): is_sheaf_iff_pairwise_intersections without products (#17181)

chore(topology/sheaf_condition): is_sheaf_iff_pairwise_intersections without products (#17181) + Generalize universes in *category_theory/limits/final* in order to generalize universe in `is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections`, from which we deduce `is_sheaf_iff_is_sheaf_pairwise_intersection` in full generality; the original version of this lemma with a `has_products` assumption now has `'` appended to its name, and will be removed in a future refactor. + As applications, we remove `has_products` from the definition of the pushforward functor in *topology/sheaves/functors* (and generalize universes there), and from skyscraper sheaves.