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.

[affeldt-aist]

I have a concern with the naming. Could we find another name for sum_fun? Something that shows that we are dealing with existT (since we have been using sum rather for bigops so far)? And maybe use the dsum prefix instead of sum to make clearer that this is not about the sumbool type?

[zstone1]

That is fair. Referencing it all as sigT might be the simplest, rather than mentioning sum at all.

[affeldt-aist]

Modulo the typo in the changelog, I can't see any issue anymore.