Following https://github.com/UniMath/agda-unimath/pull/1619#discussion_r2452677635, we should define the concept of `expansive-function-XXX`, dual of [short functions](https://unimath.github.io/agda-unimath/metric-spaces.short-functions-pseudometric-spaces.html), i.e. neighborhood-reflecting maps.