Commit 2024-01-09 21:58 4a55c95f

refactor(CategoryTheory/Sites): sheafification as an abstract left adjoint (#9012) We define a typeclass HasSheafify which says that presheaves on a site with values in some category can be sheafified, i.e. that the inclusion functor from sheaves to presheaves has a left exact left adjoint. We redefine presheafToSheaf as an arbitrary choice of such a left adjoint.