Preambles put up for Quests0,1,2; feedbackG edits

1FundamentalGroup/Preambles/P0.agda

@@ -0,0 +1,9 @@
+module 1FundamentalGroup.Preambles.P0 where
+
+open import Cubical.Data.Empty public
+open import Cubical.Data.Unit renaming ( Unit to ⊤ ) public
+open import Cubical.Data.Bool public
+open import Cubical.Foundations.Prelude renaming ( subst to endPt ) public
+open import Cubical.Foundations.Isomorphism renaming ( Iso to _≅_ ) public
+open import Cubical.Foundations.Path public
+open import Cubical.HITs.S1 public

1FundamentalGroup/Preambles/P1.agda

@@ -0,0 +1,9 @@
+module 1FundamentalGroup.Preambles.P1 where
+
+open import Cubical.HITs.S1 public
+open import Cubical.Data.Nat using (ℕ ; suc ; zero) public
+open import Cubical.Data.Int using (ℤ ; pos ; negsuc) public
+open import Cubical.Data.Empty public
+open import Cubical.Foundations.Prelude public
+open import Cubical.Foundations.HLevels public
+open import 1FundamentalGroup.Quest0Solutions using ( Refl ; Refl≢loop ) public

1FundamentalGroup/Preambles/P2.agda

@@ -0,0 +1,8 @@
+module 1FundamentalGroup.Preambles.P2 where
+
+open import Cubical.Data.Nat public
+open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_) public
+open import Cubical.Foundations.Isomorphism public
+open import Cubical.Foundations.Prelude renaming (subst to endPt) public
+open import Cubical.HITs.S1 using (S¹ ; base ; loop) public
+open import 1FundamentalGroup.Quest1 public

1FundamentalGroup/Quest0.agda

@@ -1,12 +1,6 @@
 module 1FundamentalGroup.Quest0 where
 
-open import Cubical.Data.Empty
-open import Cubical.Data.Unit renaming ( Unit to ⊤ )
-open import Cubical.Data.Bool
-open import Cubical.Foundations.Prelude renaming ( subst to endPt )
-open import Cubical.Foundations.Isomorphism renaming ( Iso to _≅_ )
-open import Cubical.Foundations.Path
-open import Cubical.HITs.S1
+open import 1FundamentalGroup.Preambles.P0
 
 Refl : base ≡ base
 Refl = {!!}

1FundamentalGroup/Quest1.agda

@@ -1,13 +1,6 @@
 module 1FundamentalGroup.Quest1 where
 
-open import Cubical.Core.Everything
-open import Cubical.HITs.S1
-open import Cubical.Data.Nat
-open import Cubical.Data.Int
-open import Cubical.Data.Empty
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-open import 1FundamentalGroup.Quest0Solutions using ( Refl ; Refl≢loop )
+open import 1FundamentalGroup.Preambles.P1
 
 Ω : (A : Type) (a : A) → Type
 Ω A a = a ≡ a 

1FundamentalGroup/Quest2.agda

@@ -1,12 +1,6 @@
 module 1FundamentalGroup.Quest2 where
 
-open import Cubical.Core.Everything
-open import Cubical.Data.Nat
-open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_)
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Prelude renaming (subst to endPt)
-open import Cubical.HITs.S1 using (S¹ ; base ; loop)
-open import 1FundamentalGroup.Quest1
+open import 1FundamentalGroup.Preambles.P2
 
 sucℤ : ℤ → ℤ
 sucℤ (pos n) = pos (suc n)
@@ -41,7 +35,7 @@ helix base = ℤ
 helix (loop i) = sucℤPath i
 
 spinCountBase : base ≡ base → ℤ
-spinCountBase p = endPt helix p 0
+spinCountBase p = endPt helix p (pos zero)
 
 spinCount : (x : S¹) → base ≡ x → helix x
-spinCount x p = endPt helix p 0
+spinCount x p = endPt helix p (pos zero)

1FundamentalGroup/feedbackG.md

@@ -2,43 +2,43 @@
 
 ## Subject info
 
-- has some experience with type theory and haskell
+[] has some experience with type theory and haskell
 
 ## Quest0/Part0
 
-- clarify the notation `a : A`
-- hide the imports
-- definition of inductive type doesn't make sense
+[x] clarify the notation `a : A`
+[x] hide the imports
+[x] definition of inductive type doesn't make sense
   without the further details.
-- confusion of `{!!}` and `{0}` and `?`
-- comparing holes to agda-info window is intuitive
-- error on firsts refine
-- add at each step what the agda-info window looks like
-- confusion about hole numbers. "just ignore them"
-- subject tries to read constraint in agda-info window. 
-  Shld deal with this somehow.
-- emphasize no need to fill holes in order.
+[x] confusion of `{!!}` and `{0}` and `?`
+[x] comparing holes to agda-info window is intuitive
+[x] error on firsts refine
+[x] add at each step what the agda-info window looks like
+[x] confusion about hole numbers. "just ignore them"
+[x] subject tries to read constraint in agda-info window. 
+    Shld deal with this somehow.
+[] emphasize no need to fill holes in order.
   
 ## Quest0/Part1
 
-- subject confused about 'space of spaces'.
+[x] subject confused about 'space of spaces'.
   More specifically, need to say `a : A` means "`a` is a point of the space `A`".
-- we shld say `a ≡ b` means space of paths from `a` to `b`.
-- 'contradiction' is a pre-existing concept in subject brain.
-- "not sure that helps" - subject about definition of `Bool`
-- "is `flipPath` taking a point from `Bool` to another point of `Bool`
+[x] we shld say `a ≡ b` means space of paths from `a` to `b`.
+[-] 'contradiction' is a pre-existing concept in subject brain.
+[] "not sure that helps" - subject about definition of `Bool`
+[] "is `flipPath` taking a point from `Bool` to another point of `Bool`
   or is it taking a space to another space?"
-- "just some terminology" - subject on the definition of _fiber_.
+[] "just some terminology" - subject on the definition of _fiber_.
   Subject did not take in the picture of what it is called fiber.
-- need to add earlier how to check goal of holes.
-- need to be clear _we are assuming `flipPath` is constructed already_.
-- overall : need to be clearer that `Type` is space of spaces,
+[] need to add earlier how to check goal of holes.
+[] need to be clear _we are assuming `flipPath` is constructed already_.
+[] overall : need to be clearer that `Type` is space of spaces,
   and paths in `Type` are saying which spaces are the same.
 
 ## Quesst0/Part2
 
-- For the `iso` bit, change to just `C-c C-r` cuz `Iso` only has one constructor.
-- say you can check def of `Iso` by using `SPC c d`
-- say "just write `s` and `r` and write the rest then load".
-- emphasize agda is indentation sensitive.
-- subject unexpectedly extracts lemma `true ≡ true`.
+[] For the `iso` bit, change to just `C-c C-r` cuz `Iso` only has one constructor.
+[] say you can check def of `Iso` by using `SPC c d`
+[] say "just write `s` and `r` and write the rest then load".
+[] emphasize agda is indentation sensitive.
+[] subject unexpectedly extracts lemma `true ≡ true`.