diff --git a/1FundamentalGroup/Quest0.agda b/1FundamentalGroup/Quest0.agda index 520eaa7..16157d0 100644 --- a/1FundamentalGroup/Quest0.agda +++ b/1FundamentalGroup/Quest0.agda @@ -6,109 +6,25 @@ 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 - -data S¹ : Type where - base : S¹ - loop : base ≡ base +open import Cubical.HITs.S1 Refl : base ≡ base -Refl = λ i → base - -{- transport - -To follow a point in `a : A` along a path `p : A ≡ B` -we use - - transport : {A B : Type u} → A ≡ B → A → B - -Why do we propify? Discuss. - --} +Refl = {!!} Flip : Bool → Bool -Flip false = true -Flip true = false +Flip x = {!!} --- notice we used `refl` instead of `λ i → false`, --- you might want to find out what `refl` does --- by looking up the definition flipIso : Bool ≅ Bool -flipIso = iso Flip Flip s r where - s : section Flip Flip - s false = refl - s true = refl - - r : retract Flip Flip - r false = refl - r true = refl +flipIso = {!!} flipPath : Bool ≡ Bool -flipPath = isoToPath flipIso +flipPath = {!!} -{- bundle over S¹ - -We want to construct a bundle over S¹ -that looks like this: --- insert image of double cover - -to do so we use flipPath -to specify the fibers of the bundle -at each point on the `loop`. -These fibers must coincide at the end-points -with the fiber we set for `base`, which is `Bool`. - --} - --- the bundle doubleCover : S¹ → Type -doubleCover base = Bool -doubleCover (loop i) = flipPath i -{- subst - -Given a bundle `B : A → Type u` -over a space `A` and a path `p : x ≡ y` -between points in `x y : A`, - - subst : (B : A → Type u) (p : x ≡ y) → B x → B y - -follows the path _over_ `p`, taking one -end point of the path in fiber `B x` to -the other end point in fiber `B y`. - -We use `subst` to get a function that takes a path `p : base ≡ base` -and follows the point `true` in the fiber `doubleCover base` -along the path over `p` to some point in `doubleCover base`. - -Note that `doubleCover base` is just `Bool` (externally). - --} +doubleCover x = {!!} endPtOfTrue : (p : base ≡ base) → doubleCover base -endPtOfTrue p = endPt doubleCover p true - -{- - -You can check that `SubstTrue Refl` and `SubstTrue loop` -are using `C-c C-n` - --} - -{- cong - -Given a function `f : A → B` -and a path `p : x ≡ y` between points `x y : A` - - cong : (f : A → B) → (p : x ≡ y) → f x ≡ f y - -gives us a path in `B` from `f x` to `f y` - -We can use the above to get the contradiction we want -by - -- assuming `p : Refl ≡ loop` -- deducing `SubstTrue Refl ≡ SubstTrue loop` using `cong` - --} +endPtOfTrue p = {!!} Refl≢loop : Refl ≡ loop → ⊥ -Refl≢loop p = true≢false (cong endPtOfTrue p) +Refl≢loop p = {!!} diff --git a/1FundamentalGroup/Quest0Part0.md b/1FundamentalGroup/Quest0Part0.md index 7556e89..d2cb5ca 100644 --- a/1FundamentalGroup/Quest0Part0.md +++ b/1FundamentalGroup/Quest0Part0.md @@ -48,7 +48,13 @@ follows the format of An "edge" is the same as a path. There are other paths in `S¹`, for example the _constant path at `base`_. -In `1FundamentalGroup/Quest0.agda` locate `Refl : base ≡ base`, +In `1FundamentalGroup/Quest0.agda` naviage to + +```agda +Refl : base ≡ base +Refl = {!!} +``` + we will guide you through defining it. We are about to construct a path `Refl : base ≡ base` (read path `Refl` from `base` to `base`) diff --git a/1FundamentalGroup/Quest0Part1.md b/1FundamentalGroup/Quest0Part1.md index f8153dd..1c5ca9b 100644 --- a/1FundamentalGroup/Quest0Part1.md +++ b/1FundamentalGroup/Quest0Part1.md @@ -70,7 +70,7 @@ define `doubleCover`. you have loaded the file with `C-c C-l`. ```agda doubleCover : S¹ → Type - doubleCover x = ? + doubleCover x = {!!} ``` - Navigate your cursor to the hole, write `x` and do `C-c C-c`. diff --git a/1FundamentalGroup/Quest0Solutions.agda b/1FundamentalGroup/Quest0Solutions.agda new file mode 100644 index 0000000..5ed9fea --- /dev/null +++ b/1FundamentalGroup/Quest0Solutions.agda @@ -0,0 +1,41 @@ +module 1FundamentalGroup.Quest0Solutions 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 + +Refl : base ≡ base +Refl = λ i → base + +Flip : Bool → Bool +Flip false = true +Flip true = false + +-- notice we used `refl` instead of `λ i → false`, +-- more on `refl` in Quest1 +flipIso : Bool ≅ Bool +flipIso = iso Flip Flip s r where + s : section Flip Flip + s false = refl + s true = refl + + r : retract Flip Flip + r false = refl + r true = refl + +flipPath : Bool ≡ Bool +flipPath = isoToPath flipIso + +doubleCover : S¹ → Type +doubleCover base = Bool +doubleCover (loop i) = flipPath i + +endPtOfTrue : (p : base ≡ base) → doubleCover base +endPtOfTrue p = endPt doubleCover p true + +Refl≢loop : Refl ≡ loop → ⊥ +Refl≢loop p = true≢false (cong endPtOfTrue p) diff --git a/1FundamentalGroup/Quest1.agda b/1FundamentalGroup/Quest1.agda index 1a7bf8e..597585a 100644 --- a/1FundamentalGroup/Quest1.agda +++ b/1FundamentalGroup/Quest1.agda @@ -4,7 +4,10 @@ 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.Quest0 using ( Refl ; Refl≢loop ) Ω : (A : Type) (a : A) → Type Ω A a = a ≡ a @@ -14,3 +17,9 @@ 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/1FundamentalGroup/Quest1Part0.md b/1FundamentalGroup/Quest1Part0.md index ec5d6ed..769aecd 100644 --- a/1FundamentalGroup/Quest1Part0.md +++ b/1FundamentalGroup/Quest1Part0.md @@ -21,7 +21,7 @@ In general the _loop space_ of a space `A` at a point `a` is defined as follows Clearly for each integer `n : ℤ` we have a path that is '`loop` around `n` times'. -Locate `loop_times` in the `Quest1.agda` +Locate `loop_times` in `1FundamentalGroup/Quest1.agda` (note how `agda` treats underscores) ```agda @@ -91,100 +91,3 @@ You can use it to find out the definition of `ℤ` and `ℕ`.

- - - -Warning : -the loop space can contain higher homotopical information that -the fundamental group does not capture. -For example, consider `S²`. -```agda -data S² : Type where - base : S² - loop : base ≡ base - northHemisphere : loop ≡ refl - southHemisphere : refl ≡ loop -``` - -

-

-What is `refl`? - -For any space `A` and point `a : A`, -`refl` is the constant path at `a`. -Technically speaking, we should write `refl a` to indicate the point we are at, -however `agda` is often smart enough to figure that out. -
-

- -Intuitively, all loops in `S²` based at `base` is homotopic to -the constant path `refl`. -In other words, the fundamental group at `base` of `S²` is trivial. -However, the 'composition' of the path `southHemisphere` with `northHemisphere` -in `base ≡ base` gives the surface of `S²`, -which intuitively is not homotopic to the constant point `base`. -So `base ≡ base` has non-trivial path structure. - -S2 - -Let's be more precise about homotopical data : -We can check that a space is 'homotopically trivial' (h-trivial) -from dimension `n` -by checking if spheres of dimension `n` can be filled. -To be h-trivial from `0` is for any two points -to have a line in between; to fill `S⁰`. -This data is captured in - -```agda -isProp : Type → Type -isProp A = (x y : A) → x ≡ y -``` - -

-

-All maps are continuous in HoTT - -There is a subtlety in the definition `isProp`. -This is _stronger_ than saying that the space `A` is path connected. -Since `A` is equipped with a continuous map taking pairs `x y : A` -to a path between them. - -We will show that `isProp S¹` is _empty_ despite `S¹` being path connected. - -
-

- -Similarly, to be h-trivial from `1` is for any two points `x y : A` -and any two paths `p q : x ≡ y` to have a homotopy from `p` to `q`; -to fill `S¹`. This is captured in - -```agda -isSet : Type → Type -isSet A = (x y : A) → isProp (x ≡ y) -``` - -We may therefore want to remove homotopical data -beyond a certain dimension. -We define the fundamental group to be -the homotopical data of `S¹` up to (and -including) dimension `1`, i.e. -the homotopical data of the loop space of `S¹` -up to dimension `0`. - -We make the definitions for a space to -have homotopical data only up to dimension `0` -and `1` respectively - - -```agda -isProp : Type → Type -isProp A = (x y : A) → x ≡ y - -isSet : Type → Type -isSet A = (x y : A) → isProp (x ≡ y) - -isProp→isSet : (A : Type) → isProp A → isSet A -``` diff --git a/1FundamentalGroup/Quest1Part1.md b/1FundamentalGroup/Quest1Part1.md new file mode 100644 index 0000000..d000a1a --- /dev/null +++ b/1FundamentalGroup/Quest1Part1.md @@ -0,0 +1,129 @@ + + +The loop space can contain higher homotopical information that +the fundamental group does not capture. +For example, consider `S²`. +```agda +data S² : Type where + base : S² + loop : base ≡ base + northHemisphere : loop ≡ refl + southHemisphere : refl ≡ loop +``` + +

+

+What is `refl`? + +For any space `A` and point `a : A`, +`refl` is the constant path at `a`. +Technically speaking, we should write `refl a` to indicate the point we are at, +however `agda` is often smart enough to figure that out. +
+

+ +Intuitively, all loops in `S²` based at `base` is homotopic to +the constant path `refl`. +In other words, the fundamental group at `base` of `S²` is trivial. +However, the 'composition' of the path `southHemisphere` with `northHemisphere` +in `base ≡ base` gives the surface of `S²`, +which intuitively is not homotopic to the constant point `base`. +So `base ≡ base` has non-trivial path structure. + +S2 + +Let's be more precise about homotopical data : +We can check that a space is 'homotopically trivial' (h-trivial) +from dimension `n` +by checking if spheres of dimension `n` can be filled. +To be h-trivial from `0` is for any two points +to have a line in between; to fill `S⁰`. +This data is captured in + +```agda +isProp : Type → Type +isProp A = (x y : A) → x ≡ y +``` + +

+

+All maps are continuous in HoTT + +There is a subtlety in the definition `isProp`. +This is _stronger_ than saying that the space `A` is path connected. +Since `A` is equipped with a continuous map taking pairs `x y : A` +to a path between them. + +We will show that `isProp S¹` is _empty_ despite `S¹` being path connected. + +
+

+ +Similarly, to be h-trivial from dimension `1` is for any two points `x y : A` +and any two paths `p q : x ≡ y` to have a homotopy from `p` to `q`; +to fill `S¹`. This is captured in + +```agda +isSet : Type → Type +isSet A = (x y : A) → isProp (x ≡ y) +``` + +To define the fundamental group we will make the loop space satisfy +`isSet` by _trucating_ the loop space'. +First we show that `isProp S¹` and `isSet S¹` are both empty. +Locate `¬isSetS¹` in `1FundamentalGroup/Quest1.agda`. +In the cubical library we have the result + +```agda +isProp→isSet : (A : Type) → isProp A → isSet A +``` + +

+

+HLevel + +Generalisation to HLevel and isHLevel n → isHLevel suc n?? + +
+

+ + +which we will not prove. +Use `isProp→isSet` to conclude `¬isPropS¹` (using `¬isSetS¹`), +from now you should fill in the hypotheses of the proof yourself +(put `h` before the `=` sign or use `C-c C-r`). + +Turning our attention to `¬isSetS¹`, +again supposing `h : isSet S¹` - +a map continuously taking each pair `x y : A` +to a point in `isProp (x ≡ y)`. +We can apply `h` twice to the only point `base` available to us, +obtaining a point of `isProp (base ≡ base)`. +Can we map this into the empty space? + +

+

+Hint 0 + +We have already shown that `Refl ≡ loop` is the empty space. +We have imported `Quest0` for you, so you can just quote the +result from there. + +
+

+ +

+

+Hint 1 + +- assume `h` +- type `Refl≢loop` it in the hole and refine +- it should now be asking for a proof that `Refl ≡ loop` +- try to use `h` + +
+

+ diff --git a/1FundamentalGroup/images/S2.png b/1FundamentalGroup/images/S2.png new file mode 100644 index 0000000..a9e6cdc Binary files /dev/null and b/1FundamentalGroup/images/S2.png differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai index f035d4c..f3f0ab2 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai new file mode 100644 index 0000000..546998d Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai index 13f7e83..a290c7c 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest1.agdai differ