Commit 2024-05-17 17:05 32139819

feat(CategoryTheory/Sites): the category of sheaves is a localization of the category of presheaves (#12374) In this PR, it is shown that the category of sheaves Sheaf J A is a localization of the category Presheaf J A with respect to the class J.W of morphisms of presheaves which become isomorphisms after applying the sheafification functor.