Commit 2021-10-14 07:51 8d67d9ae

chore(category_theory/sites/*): Generalize universes (#9675) This generalizes the universe levels for sheaves to some extent. This will allow us to now consider sheaves on C : Type u (satisfying [category.{v} C] and endowed with a Grothendieck topology) taking values in an arbitrary category with no additional universe restrictions. The only part of the theory which has not been generalized is the equivalence of the sheaf condition with the condition involving Yoneda. To generalize this would require composing with ulift_functors's, which we may or may not want to do.