Commit 2024-02-10 10:41 fa90a960
View on Github →chore(CategoryTheory/Sites): reorganise the material related to the coherent, regular and extensive topologies (#9944)
This PR adds essentially no new material (except the names regularTopology and extensiveTopology which were missing). It only reorganises the material that was previously in CategoryTheory/Sites/Coherent/Basic and CategoryTheory/Sites/Coherent/RegularExtensive, spreading it across six files in the Coherent folder.
- depends on: #9920