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
.