moved quest 2 to quest 1

1FundamentalGroup/Quest1.agda

@@ -3,10 +3,10 @@ module 1FundamentalGroup.Quest1 where
 open import 1FundamentalGroup.Preambles.P1
 
 
-Ω : (A : Type) (a : A) → Type
+loopSpace : (A : Type) (a : A) → Type
-Ω A a = a ≡ a
+loopSpace A a = a ≡ a
 
-loop_times : ℤ → Ω S¹ base
+loop_times : ℤ → loopSpace S¹ base
 loop n times = {!!}
 
 {-

1FundamentalGroup/Quest1Solutions.agda

@@ -3,10 +3,10 @@ module 1FundamentalGroup.Quest1Solutions where
 open import 1FundamentalGroup.Preambles.P1
 
 
-Ω : (A : Type) (a : A) → Type
+loopSpace : (A : Type) (a : A) → Type
-Ω A a = a ≡ a
+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