feat(topology/sheaves): sheafification (#3937)
# Sheafification of `Type` valued presheaves
We construct the sheafification of a `Type` valued presheaf,
as the subsheaf of dependent functions into the stalks
consisting of functions which are locally germs.
We show that the stalks of the sheafification are isomorphic to the original stalks,
via `stalk_to_fiber` which evaluates a germ of a dependent function at a point.
We construct a morphism `to_sheafify` from a presheaf to (the underlying presheaf of)
its sheafification, given by sending a section to its collection of germs.
## Future work
Show that the map induced on stalks by `to_sheafify` is the inverse of `stalk_to_fiber`.
Show sheafification is a functor from presheaves to sheaves,
and that it is the left adjoint of the forgetful functor.
Co-authored-by: Reid Barton <rwbarton@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
