Commit 2022-02-17 07:43 a355d88c

feat(topology/metric_space/gluing): metric space structure on sigma types (#11965) We define a (noncanonical) metric space structure on sigma types (aka arbitrary disjoint unions), as follows. Each piece is isometrically embedded in the union, while for x and y in different pieces their distance is dist x x0 + 1 + dist y0 y, where x0 and y0 are basepoints in the respective parts. This is not registered as an instance. This definition was already there for sum types (aka disjoint union of two pieces). We also fix this existing definition to avoid inhabited assumptions.