diff --git a/1FundamentalGroup/Quest0.agda b/1FundamentalGroup/Quest0.agda
index 0d0bae6..869e257 100644
--- a/1FundamentalGroup/Quest0.agda
+++ b/1FundamentalGroup/Quest0.agda
@@ -17,7 +17,7 @@ flipPath = {!!}
 doubleCover : S¹ → Type
 doubleCover x = {!!}
 
-endPtOfTrue : (p : base ≡ base) → doubleCover base
+endPtOfTrue : base ≡ base → doubleCover base
 endPtOfTrue p = {!!}
 
 Refl≢loop : Refl ≡ loop → ⊥
diff --git a/1FundamentalGroup/Quest0Solutions.agda b/1FundamentalGroup/Quest0Solutions.agda
index 2002e49..5415de5 100644
--- a/1FundamentalGroup/Quest0Solutions.agda
+++ b/1FundamentalGroup/Quest0Solutions.agda
@@ -28,7 +28,7 @@ doubleCover : S¹ → Type
 doubleCover base = Bool
 doubleCover (loop i) = flipPath i
 
-endPtOfTrue : (p : base ≡ base) → doubleCover base
+endPtOfTrue : base ≡ base → doubleCover base
 endPtOfTrue p = endPt doubleCover p true
 
 Refl≢loop : Refl ≡ loop → ⊥