Commit 2025-01-10 20:24 45970a9b
View on Github →chore(CategoryTheory): moving/renaming Subpresheaf (#20583)
From the file CategoryTheory.Sites.Subsheaf, the general definitions and properties of subpresheaves (of types) are moved to a new file Category.Subpresheaf.Basic, and it is renamed Subpresheaf instead of GrothendieckTopology.Subpresheaf.
There will be subsequent PRs developing this notion, and it will be used in the context of simplicial sets.