Commit 2020-10-29 19:28 2c7efdfc

feat(category_theory/sites): Grothendieck topology on a space (#4819) The grothendieck topology associated to a topological space. I also changed a definition I meant to change in #4816, and updated the TODOs of some docstrings; I can split these into separate PRs if needed but I think all the changes are quite minor