Contractible spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file, we define
contractible_space, a space that is homotopy equivalent to
A map is nullhomotopic if it is homotopic to a constant map.
A contractible space is one that is homotopy equivalent to
Instances of this typeclass