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

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