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.

Estimated changes