Commit 2020-10-12 23:17 d1bb5ea6

feat(topology/category/Compactum): Compact Hausdorff spaces (#4555) This PR provides the equivalence between the category of compact Hausdorff topological spaces and the category of algebras for the ultrafilter monad.

Notation

1. Compactum is the category of algebras for the ultrafilter monad. It's a wrapper around monad.algebra (of_type_functor $ ultrafilter).
2. CompHaus is the full subcategory of Top consisting of topological spaces which are compact and Hausdorff.