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 #1340
• The current PR for locally compact -> completely regular #1331
• 100 lines: The topologies (X * Y) *Z and X * (Y * Z) are homeomorphic. As are X * Y vs. Y * X #1367
• 100 lines: min/max are continuous in the order topology #1387
• 50 lines: The evaluation map (X -> Y) * X -> Y and composition map (Y -> Z) * (X -> Y) -> (X -> Z) are continuous (#1388)
• 100 lines: A topology on {i & X i}. The sum or coproduct topology #1368
• 200 lines: With the preliminary results above done, we finally start actual homotopy with "the wedge sum" #1384
• 200 lines: defining wedge_fun, that is lifting functions from {i : X i} into functions from the wedge #1398
• 200 lines: BiPointed spaces, and chaining paths #1400
• 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