class PiBase.WeaklyContractibleSpace (X : Type u) [TopologicalSpace X] : Prop

• nonempty : Nonempty X
• homotopically_trivial (x : X) (N : Type) : Finite N → Subsingleton (HomotopyGroup N X x)