Commit 2021-11-12 11:49 b51335c4

feat(category_theory/sites/plus): P⁺ for a presheaf P. (#10284) This file adds the construction of P⁺, for a presheaf P : Cᵒᵖ ⥤ D, whenever C has a Grothendieck topology J and D has the appropriate (co)limits. Later, we will show that P⁺⁺ is the sheafification of P, under certain additional hypotheses on D. See https://stacks.math.columbia.edu/tag/00W1