diff --git a/1FundamentalGroup/Quest0.agda b/1FundamentalGroup/Quest0.agda
new file mode 100644
index 0000000..6c9b8db
--- /dev/null
+++ b/1FundamentalGroup/Quest0.agda
@@ -0,0 +1,21 @@
+module 1FundamentalGroup.Quest0 where
+
+open import Cubical.Core.Everything
+open import Cubical.Data.Empty
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.GroupoidLaws
+
+data S¹ : Type where
+  base : S¹
+  loop : base ≡ base
+
+¬ : Type → Type
+¬ A = A → ⊥
+
+doubleCover : type
+doubleCover = ?
+
+
+refl≢loop : ¬ ( refl ≡ loop )
+refl≢loop h = {!!}
diff --git a/1FundamentalGroup/Quest0.md b/1FundamentalGroup/Quest0.md
new file mode 100644
index 0000000..36f5a69
--- /dev/null
+++ b/1FundamentalGroup/Quest0.md
@@ -0,0 +1,29 @@
+Whoa very cool
+=======================
+
+In this series of quests we will prove that the fundamental group
+of `S¹` is `ℤ`.
+In fact, our strategy will also show that the higher homotopy groups of
+`S¹` are all trivial. 
+We begin by formalising the problem statement.
+
+
+
+## The Circle
+
+A contruction of 'the circle' is :
+
+- a point
+- an edge from that point to itself
+
+Here is our definition of the circle in `agda`.
+
+```agda
+data S¹ : Type where
+  base : S¹
+  loop : base ≡ base
+```
+
+The `base \== base` is the _space of paths from `base` to `base`_.
+An "edge" is the same as a path.
+
diff --git a/1FundamentalGroup/pi1S1.md b/1FundamentalGroup/pi1S1.md
new file mode 100644
index 0000000..dc51339
--- /dev/null
+++ b/1FundamentalGroup/pi1S1.md
@@ -0,0 +1,33 @@
+Fundamental Group of S¹
+================
+
+Prerequisites :
+- circle 
+- loop space
+- have useless maps S¹ → ℤ and ℤ → S¹
+
+
+
+
+- we make helix from ℤ ≡ ℤ
+
+- 
+
+Motivating Steps :
+0. After sufficient pondering, you guess that
+   loops are determined by how many times they go around
+1. Count number of times loops go around using ℤ
+   by setting the single loop to +1.
+2. You can make a comparison maps between loop space and ℤ
+   but can't yet show an equivalence
+3. You realize you need to use the definition of S¹,
+   so you go from `base ≡ base ≃ Z` to  `base ≡ x ≃ Bundle x`.
+   i.e. You try to make the equivalence _over_ S¹
+
+
+Random thought : 
+to prove `a = b`, we realise that `a = f(x0)` 
+and `b = g(x0)` for `x0 : X`,
+and instead show `(x : X) → f x = g x`.
+This turns out to be easier since we now get 
+access to the recursor of `X`.
diff --git a/Plan.org b/Plan.org
index c819cdf..b37660a 100644
--- a/Plan.org
+++ b/Plan.org
@@ -100,7 +100,18 @@
 + Membership not the same as :
   + typing is unique (doesn't make sense to intersect two types)
   +
-+ Though set theory had fewer axioms type theory's assumptions are more intuitive (hence intionistic type theory)
-  There is no fiddling about with membership to construct things e.g. cartesian product
-+ 'we cannot use LEM' ~ not assuming law of excluded middle _globally_ means type theory theorems are stronger!
-+
++ Though set theory had fewer axioms type theory's assumptions are
+  more intuitive (hence intionistic type theory).
+  There is no fiddling about with membership to construct things
+  e.g. cartesian product
++ 'we cannot use LEM' ~ not assuming law of excluded middle _globally_ means
+  type theory theorems are stronger!
+
+**  Fundamental group of S1
++ def of S¹
++ a bunch of stuff about ℤ
++ isoToPath to make ℤ ≡ ℤ
++ subst
++ funExt
++ set-truncation
++ paths as equality
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai
new file mode 100644
index 0000000..c9eca07
Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai differ