Theorem topological_space.opens.map_id_inv_app

chore(topology/category/Top/opens): module-doc, cleanup, and construct some morphisms (#3601)

feature(category_theory/instances/Top/open[_nhds]): category of open sets, and open neighbourhoods of a point (merge #920 first) (#922) …