mathlib3

b51335c4 - feat(category_theory/sites/plus): `P⁺` for a presheaf `P`. (#10284)

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