Complete 1FundamentalGroup/Quest1.agda

1FundamentalGroup/Quest1.agda

@@ -7,29 +7,44 @@ loopSpace : (A : Type) (a : A) → Type
 loopSpace A a = a ≡ a
 
 loop_times : ℤ → loopSpace S¹ base
-loop n times = {!!}
+loop pos zero times = refl
+loop pos (suc n) times = loop ∙ loop (pos n) times
+loop negsuc zero times = sym loop
+loop negsuc (suc n) times = sym loop ∙ loop (negsuc n) times
 
-{-
-The definition of sucℤ goes here.
--}
 
-{-
-The definition of predℤ goes here.
--}
+sucℤ : ℤ → ℤ
+sucℤ (pos n) = pos (suc n)
+sucℤ (negsuc zero) = pos zero
+sucℤ (negsuc (suc n)) = negsuc n
 
-{-
-The definition of sucℤIso goes here.
--}
+predℤ : ℤ → ℤ
+predℤ (pos zero) = negsuc zero
+predℤ (pos (suc n)) = pos n
+predℤ (negsuc n) = negsuc (suc n)
 
-{-
-The definition of sucℤPath goes here.
--}
+sucℤIso : ℤ ≅ ℤ
+sucℤIso = iso sucℤ predℤ leftInv rightInv where
+
+  leftInv : section sucℤ predℤ
+  leftInv (pos zero) = refl
+  leftInv (pos (suc n)) = refl
+  leftInv (negsuc n) = refl
+
+  rightInv : retract sucℤ predℤ
+  rightInv (pos n) = refl
+  rightInv (negsuc zero) = refl
+  rightInv (negsuc (suc n)) = refl
+
+sucℤPath : ℤ ≡ ℤ
+sucℤPath = isoToPath sucℤIso
 
 helix : S¹ → Type
-helix = {!!}
+helix base = ℤ
+helix (loop i) = sucℤPath i
 
 windingNumberBase : base ≡ base → ℤ
-windingNumberBase = {!!}
+windingNumberBase p = endPt helix p (pos zero)
 
 windingNumber : (x : S¹) → base ≡ x → helix x
-windingNumber = {!!}
+windingNumber x p = endPt helix p (pos zero)