feat(topology/sheaves): Induced map on stalks (#7092)
This PR defines stalk maps for morphisms of presheaves. We prove that a morphism of type-valued sheaves is an isomorphism if and only if all the stalk maps are isomorphisms.
A few more lemmas about unique gluing are also added, as well as docstrings.
