adding the sum topology

[zstone1]

Another preliminary for #1350, this adds the very basic topology for sums. There are a lot of results about sums that are missing, of course. Sums preserve uniform and pseudometric structures, and basically all the local properties. But for now I just provide what I need for homotopy theory.

Annoyingly, there is a call to the non-ssreflect tactic destruct here, when dealing with dependent equalities. When I have a fact that i = j, then form existT P i x = existT P j y should produce a x = y. I could not figure how to do this. If the destruct tactic is forbidden, then how should I remove it?

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]

What is really not recommended is to let destruct figure out names itself but indeed we can do without it as shown in the last commit.