Commit 2023-10-21 06:49 dac8099a

feat: universe generalizations in UniqueGluing and Forget (#7654)

• Add a criterion isLimit_iff for a cone to be a limit in Limits/Types.lean.
• Use the criterion to show the equivalence between the UniqueGluing and PairwiseIntersection sheaf conditions without going through EqualizerProducts, thereby generalize the universes.
• Remove theorems/def that are now unnecessary. (cc @justus-springer)
• Generalize isSheaf_iff_isSheaf_forget for sheaves on sites using isSheaf_iff_isLimit; use it to prove and generalize the result on topological spaces, removing a large chunk of code.