fact: Fixpoint Sphere (n : trunc_index) := match n return Type with | -2 => Empty | -1 => Empty | n'.+1 => Susp (Sphere n') end.
imports: Basics Types WildCat.Equiv NullHomotopy Homotopy.Suspension Pointed Truncations Spaces.Circle Spaces.TwoSphere