mathlib

c82b7082 - feat(category_theory/sites): the canonical topology on a category (#4928)

feat(category_theory/sites): the canonical topology on a category (#4928) Explicitly construct the finest topology for which the given presheaves are sheaves, and specialise to construct the canonical topology. Also one or two tiny changes which should have been there before