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