diff --git a/1FundamentalGroup/Quest1.agda b/1FundamentalGroup/Quest1.agda
index 4ab21d0..5b93ee6 100644
--- a/1FundamentalGroup/Quest1.agda
+++ b/1FundamentalGroup/Quest1.agda
@@ -4,16 +4,13 @@ open import 1FundamentalGroup.Preambles.P1
 
 
 Ω : (A : Type) (a : A) → Type
-Ω A a = a ≡ a 
+Ω A a = a ≡ a
 
 loop_times : ℤ → Ω S¹ base
-loop pos zero times = refl
-loop pos (suc n) times = loop pos n times ∙ loop
-loop negsuc zero times = sym loop
-loop negsuc (suc n) times = loop negsuc n times ∙ sym loop
+loop n times = {!!}
 
 ¬isSetS¹ : isSet S¹ → ⊥
-¬isSetS¹ h = Refl≢loop (h base base Refl loop)
+¬isSetS¹ = {!!}
 
 ¬isPropS¹ : isProp S¹ → ⊥
-¬isPropS¹ h = ¬isSetS¹ (isProp→isSet h)
+¬isPropS¹ = {!!}
diff --git a/1FundamentalGroup/Quest1Solutions.agda b/1FundamentalGroup/Quest1Solutions.agda
new file mode 100644
index 0000000..9fbf1ab
--- /dev/null
+++ b/1FundamentalGroup/Quest1Solutions.agda
@@ -0,0 +1,19 @@
+-- ignore
+module 1FundamentalGroup.Quest1Solutions where
+open import 1FundamentalGroup.Preambles.P1
+
+
+Ω : (A : Type) (a : A) → Type
+Ω A a = a ≡ a
+
+loop_times : ℤ → Ω S¹ base
+loop pos zero times = refl
+loop pos (suc n) times = loop pos n times ∙ loop
+loop negsuc zero times = sym loop
+loop negsuc (suc n) times = loop negsuc n times ∙ sym loop
+
+¬isSetS¹ : isSet S¹ → ⊥
+¬isSetS¹ h = Refl≢loop (h base base Refl loop)
+
+¬isPropS¹ : isProp S¹ → ⊥
+¬isPropS¹ h = ¬isSetS¹ (isProp→isSet h)
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai
new file mode 100644
index 0000000..0605090
Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai differ