diff --git a/1FundamentalGroup/Quest3Solutions.agda b/1FundamentalGroup/Quest3Solutions.agda
index 37c92cf..b999030 100644
--- a/1FundamentalGroup/Quest3Solutions.agda
+++ b/1FundamentalGroup/Quest3Solutions.agda
@@ -4,6 +4,6 @@ open import Cubical.Foundations.Prelude
 open import Cubical.HITs.S1
 open import 1FundamentalGroup.Quest1Solutions
 
-outOfS¹ : (B : S¹ → Type) → (b : B base) → b ≡ b → (x : S¹) → B x
+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!}
+outOfS¹ B b p (loop i) = p i
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai
index 6578bbb..7f2ff9f 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest3Solutions.agdai differ