fact: Definition equiv_S1_Circle : Sphere 1 <~> Circle := Build_Equiv _ _ _ isequiv_S1_to_Circle.
imports: Basics Types WildCat.Equiv NullHomotopy Homotopy.Suspension Pointed Truncations Spaces.Circle Spaces.TwoSphere