Commit 2020-07-24 17:03 47efcf3c

chore(algebraic_geometry/presheafed_space): use projection rather than fancy coercion (#3507) We'd gone to great effort when writing PresheafedSpace to create a coercion from morphisms of PresheafedSpaces to morphisms in Top. It's hard to read, it's fragile. So this PR rips out that coercion, and renames the "continuous map between base spaces" field from f to base, and uses that throughout.