diff --git a/1FundamentalGroup/Quest1SideQuests/Sn.agda b/1FundamentalGroup/Quest1SideQuests/Sn.agda new file mode 100644 index 0000000..13a5b14 --- /dev/null +++ b/1FundamentalGroup/Quest1SideQuests/Sn.agda @@ -0,0 +1,23 @@ +module 1FundamentalGroup.Quest1SideQuests.Sn where + +open import Cubical.Data.Nat +open import Cubical.Data.Empty +open import Cubical.Data.Unit renaming (Unit to ⊤) +open import Cubical.Data.Bool +open import Cubical.Foundations.Prelude + + +data susp (X : Type) : Type where + north : {!!} + south : {!!} + merid : {!!} + +Sphere : ℕ → Type +Sphere = {!!} + +Disk : (n : ℕ) → Type +Disk zero = {!!} +Disk (suc n) = {!!} + +SphereToDisk : {n : ℕ} → Sphere n → Disk n +SphereToDisk {n} s = {!!} diff --git a/1FundamentalGroup/Quest1SideQuests/SnSolutions.agda b/1FundamentalGroup/Quest1SideQuests/SnSolutions.agda new file mode 100644 index 0000000..2bbad3d --- /dev/null +++ b/1FundamentalGroup/Quest1SideQuests/SnSolutions.agda @@ -0,0 +1,28 @@ +module 1FundamentalGroup.Quest1SideQuests.SnSolutions where + +open import Cubical.Data.Nat +open import Cubical.Data.Empty +open import Cubical.Data.Unit renaming (Unit to ⊤) +open import Cubical.Data.Bool +open import Cubical.Foundations.Prelude + + +data susp (X : Type) : Type where + north : susp X + south : susp X + merid : X → north ≡ south + +Sphere : ℕ → Type +Sphere zero = Bool +Sphere (suc n) = susp (Sphere n) + +Disk : (n : ℕ) → Type +Disk zero = ⊤ +Disk (suc n) = susp (Sphere n) + +SphereToDisk : {n : ℕ} → Sphere n → Disk (suc n) +SphereToDisk {zero} false = north +SphereToDisk {zero} true = south +SphereToDisk {suc n} north = north +SphereToDisk {suc n} south = south +SphereToDisk {suc n} (merid x i) = merid (SphereToDisk x) i diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest1SideQuests/Sn.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest1SideQuests/Sn.agdai new file mode 100644 index 0000000..31d804c Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest1SideQuests/Sn.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest1SideQuests/SnSolutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest1SideQuests/SnSolutions.agdai new file mode 100644 index 0000000..fda14df Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest1SideQuests/SnSolutions.agdai differ