Simply connected spaces #

This file defines simply connected spaces. A topological space is simply connected if its fundamental groupoid is equivalent to Unit.

Main theorems #

A simply connected space is one whose fundamental groupoid is equivalent to Discrete Unit

    theorem SimplyConnectedSpace.paths_homotopic {X : Type u_1} [TopologicalSpace X] [SimplyConnectedSpace X] {x : X} {y : X} (p₁ : Path x y) (p₂ : Path x y) :
    Path.Homotopic p₁ p₂

    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.