diff --git a/1FundamentalGroup/Quest3Solutions.agda b/1FundamentalGroup/Quest3Solutions.agda
index 849ce06..8f4be97 100644
--- a/1FundamentalGroup/Quest3Solutions.agda
+++ b/1FundamentalGroup/Quest3Solutions.agda
@@ -1,21 +1,15 @@
 module 1FundamentalGroup.Quest3Solutions where
 
-open import Cubical.Foundations.Prelude
 open import Cubical.HITs.S1 using ( S¹ ; base ; loop )
 open import 1FundamentalGroup.Quest1Solutions
+open import Cubical.Foundations.Prelude renaming (transport to pathToFun)
 open import Cubical.Foundations.Path
-
-outOfS¹ : (B : S¹ → Type) → (b : B base) → PathP (λ i → B (loop i)) b b → (x : S¹) → B x
-outOfS¹ B b p base = b
-outOfS¹ B b p (loop i) = p i
-
-
+open import 0Trinitarianism.Quest5Solutions
 
 rewind : (x : S¹) → helix x → base ≡ x
-rewind base = loop_times
-rewind (loop i) = path i where
-
-   path : PathP (λ i → helix (loop i) → base ≡ loop i) loop_times loop_times
-   path  = {!!}
-
-thing = PathPIsoPath
+rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
+  (
+    pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
+  ≡⟨ {!!} ⟩
+    loop_times ∎
+  )
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai
index 7f2ff9f..bcd1697 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai differ