\import Function
\import Homotopy.Pointed
\import Homotopy.Suspension
\import Logic

\func Sphere (n : Nat) => Susp (iterr Susp n Empty)
  \where
    \func pointed (n : Nat) => \new Pointed (Sphere n) north