Commit 2020-07-22 05:08 64335decView on Github →
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
There is a slight regression in
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).