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.