mathlib

60bc370d - feat(category_theory/sites/limits): `Sheaf_to_presheaf` creates limits (#10328)

feat(category_theory/sites/limits): `Sheaf_to_presheaf` creates limits (#10328) As a consequence, we obtain that sheaves have limits (of a given shape) when the target category does, and that these limit sheaves are computed on each object of the site "pointwise".