From e6afea6d88049b94a6eb979d0599939904be908d Mon Sep 17 00:00:00 2001
From: germax26 <maximburykin1@gmail.com>
Date: Mon, 21 Jul 2025 17:44:34 +1000
Subject: [PATCH] Complete 1FundamentalGroup/Quest1.agda

---
 1FundamentalGroup/Quest1.agda | 47 +++++++++++++++++++++++------------
 1 file changed, 31 insertions(+), 16 deletions(-)

diff --git a/1FundamentalGroup/Quest1.agda b/1FundamentalGroup/Quest1.agda
index bb63b46..ccbe6f8 100644
--- a/1FundamentalGroup/Quest1.agda
+++ b/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)