Commit 2025-09-28 16:48 7a743c48

feat(CategoryTheory/Sites): some lemmas on separated presheaves (#30044) A handful of simple API lemmas on separated presheaves of types. Specifically:

• for J ≤ J' every J'-separated presheaf is J-separated
• subpresheaves of separated presheaves are separated
• a presheaf is separated iff a presheaf isomorphic to it is
• a separated presheaf for which all compatible families admit amalgamations is a sheaf. We also change the implicit binder in the definition of Presieve.IsSeparated to a strict-implicit one to enable better support for dot notation, and slightly simplify the proof of Subpresheaf.sheafify_isSheaf as an application.