Dagur Asgeirsson

--- [](https://gitpod.io/from-referrer/)

feat(LightCondensed): the functor from `TopCat`

1

--- - [ ] depends on: #10412 [](https://gitpod.io/from-referrer/)

--- [](https://gitpod.io/from-referrer/)

refactor(Topology/Category): unify some definitions of subcategories of compact Hausdorff spaces

2

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...

chore(Category/TopCat): cleanup

3

--- [](https://gitpod.io/from-referrer/)

feat(Condensed): characterisation of discrete (light) condensed sets and modules

2

This PR provides a characterisation of discrete condensed sets and modules, both in the light setting and the classical one. * A condensed module is discrete if and only if...

refactor(Topology/Category): refactor LightProfinite.Basic

2

This is the second part of the refactor of CompHaus and friends (refactoring the definition of `LightProfinite` in terms of `CompHausLike`, see #12930 for the end result) --- - [x]...

refactor(Topology/Category): refactor Stonean.Basic

2

This is the second part of the refactor of CompHaus and friends (refactoring the definition of `Stonean` in terms of `CompHausLike`, see #12930 for the end result) --- - [x]...

refactor(Topology/Category): refactor Profinite.Basic

2

This is the second part of the refactor of CompHaus and friends (refactoring the definition of `Profinite` in terms of `CompHausLike`, see #12930 for the end result) --- - [x]...

refactor(Topology/Category): refactor CompHaus.Basic

2

This PR refactors the file `CompHaus.Basic` in terms of the new `CompHausLike` API. Other files are touched only to fix errors created by this refactor, they will be refactored later...