\import Homotopy.Pointed
\import Homotopy.Pushout

\func Susp (A : \Type) => PushoutData {A} (\lam _ => ()) (\lam _ => ())
  \where {
    \func rec {A B : \Type} (b1 b2 : B) (f : A -> b1 = b2) (x : Susp A) : B \elim x
      | north => b1
      | south => b2
      | pglue a => f a

    \func pointed (A : \Type) => \new Pointed (Susp A) north

    \func pushout (A : \Type) => pushoutData {A} (\lam _ => ()) (\lam _ => ())
  }

\cons north {A : \Type} : Susp A => pinl ()

\cons south {A : \Type} : Susp A => pinr ()

\func pmerid {A : \Type} (a : A) : north = south => path (pglue a)