fundamental groupoid for homotopy theory

[zstone1]

A grab-bag of results I'll need to split into separate reviews (once topology.v's split is done). This PR is mostly for bookkeeping, and stating my (new) roadmap for homotopies. My plan for breaking things into reviewable chunks is

• continuity mixins subtypes and continuous functions #1340
• The current PR for locally compact -> completely regular completely regular spaces and locally compact implies uniform #1331
• 100 lines: The topologies (X * Y) *Z and X * (Y * Z) are homeomorphic. As are X * Y vs. Y * X Homeomorphisms for (X*Y)*Z -> X*(Y*Z) and X*Y -> Y*X #1367
• 100 lines: min/max are continuous in the order topology
• 50 lines: The evaluation map (X -> Y) * X -> Y and composition map (Y -> Z) * (X -> Y) -> (X -> Z) are continuous
• 100 lines: A topology on {i & X i}. The sum or coproduct topology adding the sum topology #1368
• 300 lines: With the preliminary results above done, we finally start actual homotopy with "the wedge sum"
• 200 lines: BiPointed spaces, and chaining paths
• 200 lines: SelfSplitting structures, and path-concatentation
• 150 lines: The PathBetween relation
• 100 lines: reparameterization and joint continuity
• 150 lines: the fundamental groupoid
• 100 lines: lifting functions from U -> V to functors on the fundamental groupoids

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels