mathlib

cf1b0ca3 - Halfway through defining coarse maps and equivalences