Commit 2021-11-15 05:07 189e0662

feat(category_theory/sites/sheafification): The sheafification of a presheaf. (#10303) We construct the sheafification of a presheaf P taking values in a concrete category D with enough (co)limits, where the forgetful functor preserves the appropriate (co)limits and reflects isomorphisms. We follow the construction on the stacks project https://stacks.math.columbia.edu/tag/00W1 Note: There are two very long proofs here, so I added several comments explaining what's going on.