Theorem category_theory.examples.comm_ring_hom.id_map

style(category_theory): concrete categories as type class

feat(category_theory): the category of topological spaces, and of neighbourhoods of a point. also the category of commutative rings