mathlib3

feat(topology/constructions): topology of sum types

#1016

Merged