Commit 2022-10-27 07:38 20e597fb

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.