Commit 2023-10-03 12:58 7afe52aa

feat: the union of the regular and extensive coverages generates the coherent topology (#6876) We define the regular and extensive coverages on categories and prove that their union generates the coherent topology on extensive, regular, precoherent categories.

• depends on: #6878
• depends on: #6879
• depends on: #6896