composition is continuous

[zstone1]

The last of the foundational bits for homotopy. The idea is simply that for nice spaces (E.G. locally compact) in the compact-open topology, composition itself is continuous. A couple small notes

• Apparently the condition of local compactness of X is unnecessary (munrkes $46, ex. 7). But the proof here is much easier, and it shouldn't matter too much for us in the near future.
• The regular_space condition is redundant due to locally_compact_completely_regular + completely_regular_regular. But those proofs sit in normed_type.v and need to be moved to separation_axioms.v before they can be used. Can be cleaned up later (or as a prerequisite if you think that's more important)

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

[affeldt-aist]

continuous_curry_joint_cvg: why not simply continuous_curry_cvg?

[zstone1]

Rename done. I'll merge once the master build is fixed.