Commit 2020-07-22 05:08 64335dec

chore(topology/category/): switch to bundled morphisms in Top (#3506) This is a natural follow-up to @Nicknamen's recent PRs splitting bundled continuous maps out of compact_open. There is a slight regression in algebraic_geometry.presheafed_space and algebraic_geometry.stalks, requiring a more explicit coercion. I'd encourage reviewers to ignore this, as I'll make a separate PR simplifying this (basically: having a coercion from morphisms of PresheafedSpaces to morphisms of Tops is unrealistically ambitious, and moreover harder to read, than just using the projection notation, and removing it makes everything easier).