open import Paths

open data Susp (A : Type)
| north
| south
| merid A : north = south

variable A B : Type
def mapSusp (A → B) (Susp A) : Susp B
| f, north ⇒ north
| f, south ⇒ south
| f, merid a i ⇒ merid (f a) i