Commit 2023-11-13 10:29 a5f84091

View on Github →

feat(CategoryTheory/Sites): the topology on Over categories (#8329) Given a Grothendieck topology on a category C, this PR constructs the induced Grothendieck topology on the category Over X for any X : C.

Estimated changes