Commit 2024-08-01 08:35 26269fbb

refactor(Topology/Category): unify some definitions of subcategories of compact Hausdorff spaces (#12930) This PR unifies the definitions of the categories CompHaus, Profinite, Stonean, and LightProfinite by defining a structure CompHausLike P depending on a predicate P on topological spaces. Many of the properties of these categories of compact Hausdorff spaces are shared between them and this approach reduces duplication of boilerplate code, in particular the explicit constructions of certain limits and colimits.