added 1FundamentalGroup

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 = {!!}

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.
+

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`.

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