Table of Contents - 20.3.14.7. Topological Manifolds

Found this and was curious about how manifolds would be expressed in set.mm:
https://mathoverflow.net/questions/336367/real-manifolds-in-a-theorem-prover

This chapter proposes to define first manifold topologies, which characterize
topological manifolds, and then to extend the structure with presentations,
i.e., equivalence classes of atlases for a given topological space. We
suggest to use the extensible structures to define the "topological space"
aspect of topological manifolds, and then extend it with
charts/presentations.