open import Arith::Bool
open import Arith::Nat::Core
open import Spaces::Susp::Core
open import Spaces::Sphere::S1::Core
open import Spaces::Sphere::S2::Core
open import Paths

def Sphere Nat : Type
| 0 ⇒ Bool
| suc n ⇒ Susp (Sphere n)

def point (n : Nat) : Sphere n
| 0 ⇒ true
| suc n ⇒ north

def Sphere1-S¹ (Sphere 1) : S¹
| merid false i ⇒ loop i
| _ ⇒ base

def S¹-Sphere1 S¹ : Sphere 1
| base ⇒ north
| loop i ⇒ (merid false <==> sym (merid true)) i

def SuspS¹-S² (Susp S¹) : S²
| merid (loop i) j ⇒ surf i j
| _ ⇒ base2