diff --git a/1FundamentalGroup/Quest1.agda b/1FundamentalGroup/Quest1.agda
index 12f972c..bb63b46 100644
--- a/1FundamentalGroup/Quest1.agda
+++ b/1FundamentalGroup/Quest1.agda
@@ -3,10 +3,10 @@ module 1FundamentalGroup.Quest1 where
 open import 1FundamentalGroup.Preambles.P1
 
 
-Ω : (A : Type) (a : A) → Type
-Ω A a = a ≡ a
+loopSpace : (A : Type) (a : A) → Type
+loopSpace A a = a ≡ a
 
-loop_times : ℤ → Ω S¹ base
+loop_times : ℤ → loopSpace S¹ base
 loop n times = {!!}
 
 {-
diff --git a/1FundamentalGroup/Quest1Solutions.agda b/1FundamentalGroup/Quest1Solutions.agda
index bb40813..b8aa0a0 100644
--- a/1FundamentalGroup/Quest1Solutions.agda
+++ b/1FundamentalGroup/Quest1Solutions.agda
@@ -3,10 +3,10 @@ module 1FundamentalGroup.Quest1Solutions where
 open import 1FundamentalGroup.Preambles.P1
 
 
-Ω : (A : Type) (a : A) → Type
-Ω A a = a ≡ a
+loopSpace : (A : Type) (a : A) → Type
+loopSpace A a = a ≡ a
 
-loop_times : ℤ → Ω S¹ base
+loop_times : ℤ → loopSpace S¹ base
 loop pos zero times = refl
 loop pos (suc n) times = loop pos n times ∙ loop
 loop negsuc zero times = sym loop
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai
index 6f595d0..3dd2981 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai differ