quest2 -> quest1

1FundamentalGroup/Preambles/P1.agda

@@ -1,9 +1,9 @@
 module 1FundamentalGroup.Preambles.P1 where
 
-open import Cubical.HITs.S1 public
+open import Cubical.HITs.S1 using (S¹ ; base ; loop) public
 open import Cubical.Data.Nat using (ℕ ; suc ; zero) public
-open import Cubical.Data.Int using (ℤ ; pos ; negsuc) public
+open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_) public
 open import Cubical.Data.Empty public
-open import Cubical.Foundations.Prelude public
+open import Cubical.Foundations.Prelude renaming (subst to endPt) public
-open import Cubical.Foundations.HLevels public
+open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public
 open import 1FundamentalGroup.Quest0Solutions using ( Refl ; Refl≢loop ) public

1FundamentalGroup/Quest1.agda

@@ -9,8 +9,27 @@ open import 1FundamentalGroup.Preambles.P1
 loop_times : ℤ → Ω S¹ base
 loop n times = {!!}
 
-¬isSetS¹ : isSet S¹ → ⊥
+{-
-¬isSetS¹ = {!!}
+The definition of sucℤ goes here.
+-}
 
-¬isPropS¹ : isProp S¹ → ⊥
+{-
-¬isPropS¹ = {!!}
+The definition of predℤ goes here.
+-}
+
+{-
+The definition of sucℤIso goes here.
+-}
+
+{-
+The definition of sucℤPath goes here.
+-}
+
+helix : S¹ → Type
+helix = {!!}
+
+windingNumberBase : base ≡ base → ℤ
+windingNumberBase = {!!}
+
+windingNumber : (x : S¹) → base ≡ x → helix x
+windingNumber = {!!}

1FundamentalGroup/Quest1Solutions.agda

@@ -12,8 +12,40 @@ loop pos (suc n) times = loop pos n times ∙ loop
 loop negsuc zero times = sym loop
 loop negsuc (suc n) times = loop negsuc n times ∙ sym loop
 
-¬isSetS¹ : isSet S¹ → ⊥
+sucℤ : ℤ → ℤ
-¬isSetS¹ h = Refl≢loop (h base base Refl loop)
+sucℤ (pos n) = pos (suc n)
+sucℤ (negsuc zero) = pos zero
+sucℤ (negsuc (suc n)) = negsuc n
 
-¬isPropS¹ : isProp S¹ → ⊥
+predℤ : ℤ → ℤ
-¬isPropS¹ h = ¬isSetS¹ (isProp→isSet h)
+predℤ (pos zero) = negsuc zero
+predℤ (pos (suc n)) = pos n
+predℤ (negsuc n) = negsuc (suc n)
+
+sucℤIso : ℤ ≅ ℤ
+sucℤIso = iso sucℤ predℤ s r where
+
+  s : section sucℤ predℤ
+  s (pos zero) = refl
+  s (pos (suc n)) = refl
+  s (negsuc zero) = refl
+  s (negsuc (suc n)) = refl
+
+  r : retract sucℤ predℤ
+  r (pos zero) = refl
+  r (pos (suc n)) = refl
+  r (negsuc zero) = refl
+  r (negsuc (suc n)) = refl
+
+sucℤPath : ℤ ≡ ℤ
+sucℤPath = isoToPath sucℤIso
+
+helix : S¹ → Type
+helix base = ℤ
+helix (loop i) = sucℤPath i
+
+windingNumberBase : base ≡ base → ℤ
+windingNumberBase p = endPt helix p (pos zero)
+
+windingNumber : (x : S¹) → base ≡ x → helix x
+windingNumber x p = endPt helix p (pos zero)

1FundamentalGroup/Shelf/questExtras.agda

@@ -0,0 +1,12 @@
+¬isSetS¹ : isSet S¹ → ⊥
+¬isSetS¹ = {!!}
+
+¬isPropS¹ : isProp S¹ → ⊥
+¬isPropS¹ = {!!}
+
+-------------solutions------
+¬isSetS¹ : isSet S¹ → ⊥
+¬isSetS¹ h = Refl≢loop (h base base Refl loop)
+
+¬isPropS¹ : isProp S¹ → ⊥
+¬isPropS¹ h = ¬isSetS¹ (isProp→isSet h)