open import Paths

open data S²
| base2
| surf (i j : I) { ∂ i ∨ ∂ j := base2 }

def ΩS² ⇒ base2 = base2
// def isContrΩS² : isContr ΩS² => (idp, {??})