Commit 2023-12-07 09:17 85fd9151

refactor(Topology): simplify proofs that CompHaus and friends are Precoherent (#8644) We prove that CompHaus and friends are Precoherent by proving that they are Preregular and FinitaryExtensive, removing the previous hacky proofs of characterisations of effective epimorphic families. We also give new, cleaner proofs of those characterisations.

• depends on: #8643