Simply connected spaces #
This file defines simply connected spaces.
A topological space is simply connected if its fundamental groupoid is equivalent to
Main theorems #
simply_connected_iff_unique_homotopic- A space is simply connected if and only if it is nonempty and there is a unique path up to homotopy between any two points
simply_connected_space.of_contractible- A contractible space is simply connected
- equiv_unit : nonempty (fundamental_groupoid X ≌ category_theory.discrete unit)
A simply connected space is one whose fundamental groupoid is equivalent to
Instances of this typeclass
In a simply connected space, any two paths are homotopic
A space is simply connected iff it is path connected, and there is at most one path up to homotopy between any two points.
Another version of