From 0b0693080a4b15d5f19d7e928dcc6202326cf234 Mon Sep 17 00:00:00 2001
From: Jlh18 <josephhua73@yahoo.com>
Date: Thu, 21 Oct 2021 14:31:36 +0100
Subject: [PATCH] endPtOfTrue

---
 1FundamentalGroup/Quest0.agda          | 2 +-
 1FundamentalGroup/Quest0Solutions.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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 → ⊥