Two related things. Now that pointed is gone from topology, we can canonically add topology/uniform/pseudometric on set_val. This now just a few easy instances.
Then we define a mixin for continuous functions. We build two structures from this. One is just Continuous for use with subtypes, and ContinuousFun for mixing with the Fun hierarchy using subspaces. And a bunch of lemmas for converting between them. Then we endow the set of continuous functions with various topologies in the ArrowAsT modules in function_spaces.v. In general I'd like to say "if arrow has a topology, then continuousType` inherits it, but I don't know how to say that in general, so it's fine to just manually do the instances in those modules.
Checklist
[ ] added corresponding entries in CHANGELOG_UNRELEASED.md
[ ] added corresponding documentation in the headers
Two related things. Now that pointed is gone from
topology, we can canonically add topology/uniform/pseudometric onset_val. This now just a few easy instances.Then we define a mixin for continuous functions. We build two structures from this. One is just
Continuousfor use with subtypes, andContinuousFunfor mixing with theFunhierarchy using subspaces. And a bunch of lemmas for converting between them. Then we endow the set of continuous functions with various topologies in theArrowAsTmodules infunction_spaces.v. In general I'd like to say "if arrow has a topology, then continuousType` inherits it, but I don't know how to say that in general, so it's fine to just manually do the instances in those modules.Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers