fact: Definition iscohhspace_s1 : IsCohHSpace (psphere 1) := Build_IsCohHSpace _ _ _.
imports: Classes.interfaces.canonical_names Cubical Homotopy.Suspension Homotopy.HSpace.Core Homotopy.HSpace.Coherent Spaces.Spheres