Commit 2024-01-13 15:06 82e1d3a9

feat(CategoryTheory): sheafification over essentially small sites (#9523) This PR provides the necessary API to sheafify over large but essentially small categories.

• Given an equivalence of categories and a Grothendieck topology on one of them, we transport the topology along the equivalence and prove that the sheaf categories are equivalent.
• We prove that the property HasSheafify transports over the equivalence of sheaf categories mentioned above, and same for the property HasSheafCompose 
• We also add instances for the existence of small limits on sheaf categories on essentially small sites.
• depends on: #9012