a bit of wip into ch6

src/HottBook/Chapter2Util.agda

@@ -2,10 +2,25 @@ module HottBook.Chapter2Util where
 
 open import HottBook.Chapter1
 open import HottBook.Chapter2
+open import HottBook.CoreUtil
 
 neg-homotopy : (neg ∘ neg) ∼ id
 neg-homotopy true = refl
 neg-homotopy false = refl
 
 neg-equiv : 𝟚 ≃ 𝟚
-neg-equiv = neg , qinv-to-isequiv (mkQinv neg neg-homotopy neg-homotopy)
+neg-equiv = neg , qinv-to-isequiv (mkQinv neg neg-homotopy neg-homotopy)
+
+Bool : ∀ {l} → Set l
+Bool = Lift 𝟚
+
+Bool-neg : ∀ {l} → Bool {l} → Bool {l}
+Bool-neg (lift true) = lift false
+Bool-neg (lift false) = lift true
+
+Bool-neg-homotopy : ∀ {l} → (Bool-neg {l} ∘ Bool-neg {l}) ∼ id
+Bool-neg-homotopy (lift true) = refl
+Bool-neg-homotopy (lift false) = refl
+
+Bool-neg-equiv : ∀ {l} → Bool {l} ≃ Bool {l}
+Bool-neg-equiv = Bool-neg , qinv-to-isequiv (mkQinv Bool-neg Bool-neg-homotopy Bool-neg-homotopy)

src/HottBook/Chapter3.lagda.md

@@ -126,30 +126,35 @@ lemma3∙1∙8 {A} A-set x y p q r s =
 ### Example 3.1.9
 
 ```
-example3∙1∙9 : ¬ (isSet Set)
+example3∙1∙9 : ∀ {l} → ¬ (isSet (Set l))
 example3∙1∙9 p = remark2∙12∙6.true≢false lol
   where
     open axiom2∙10∙3
 
-    f-path : 𝟚 ≡ 𝟚
-    f-path = ua neg-equiv
+    f-path : Bool ≡ Bool
+    f-path = ua Bool-neg-equiv
 
-    bogus : id ≡ neg
+    bogus : id ≡ Bool-neg
     bogus =
       let
         helper : f-path ≡ refl
-        helper = p 𝟚 𝟚 f-path refl
+        helper = p Bool Bool f-path refl
 
         wtf : idtoeqv f-path ≡ idtoeqv refl
         wtf = ap idtoeqv helper
 
+        wtf2 : Σ.fst (idtoeqv (ua Bool-neg-equiv)) ≡ id
         wtf2 = ap Σ.fst wtf
-        wtf3 = ap Σ.fst (propositional-computation neg-equiv)
+
+        wtf3 : Σ.fst (idtoeqv (ua Bool-neg-equiv)) ≡ Bool-neg
+        wtf3 = ap Σ.fst (propositional-computation Bool-neg-equiv)
+
+        wtf4 : Bool-neg ≡ id
         wtf4 = sym wtf3 ∙ wtf2
       in sym wtf4
 
     lol : true ≡ false
-    lol = ap (λ f → f true) bogus
+    lol = ap (λ f → Lift.lower (f (lift true))) bogus
 ```
 
 ## 3.2 Propositions as types?

src/HottBook/Chapter3Exercises.lagda.md

@@ -30,11 +30,25 @@ exercise3∙1 {A} {B} equiv@(f , mkIsEquiv g g* h h*) isSetA xB yB pB qB =
     lol3 : ap (f ∘ g) pB ≡ ap (f ∘ g) qB
     lol3 = sym (lemma2∙2∙2.iii g f pB) ∙ lol2 ∙ (lemma2∙2∙2.iii g f qB)
 
-    lemma1 : ∀ {A B} {x y : A} (f g : A → B)
-      → (p : x ≡ y) 
-      → f ≡ g
-      → ap f p ≃ {! ap g p  !}
-    lemma1 = {!   !}
+    lol4 : (xB ≡ yB) → ((f ∘ g) xB ≡ (f ∘ g) yB)
+    lol4 p = ap (f ∘ g) p
+
+    lol5 : ((f ∘ g) xB ≡ (f ∘ g) yB) → (xB ≡ yB)
+    lol5 p = sym (g* xB) ∙ p ∙ g* yB
+
+    -- lol4 : (xB ≡ yB) → ((f ∘ g) xB ≡ (f ∘ g) yB)
+    -- lol4 = ua (ff , qinv-to-isequiv (mkQinv gg forward {!   !}))
+    --   where
+    --     gg : ((f ∘ g) xB ≡ (f ∘ g) yB) → (xB ≡ yB)
+    --     gg p = sym (g* xB) ∙ p ∙ g* yB
+    --     forward : (p : (f ∘ g) xB ≡ (f ∘ g) yB) → ap (f ∘ g) (gg p) ≡ p
+    --     forward p = {!   !}
+
+    -- lemma1 : ∀ {A B} {x y : A} (f g : A → B)
+    --   → (p : x ≡ y) 
+    --   → f ≡ g
+    --   → ap f p ≃ {! ap g p  !}
+    -- lemma1 = {!   !}
 
     -- lol4 : ∀ {A B} {x y : B}
     --   → (p : x ≡ y) → (f : A → B) → (g : B → A)

src/HottBook/Chapter6.lagda.md

@@ -1,3 +1,6 @@
+<details>
+  <summary>Imports</summary>
+
 ```
 module HottBook.Chapter6 where
 
@@ -10,14 +13,11 @@ private
     l : Level
 ```
 
+</details>
+
 # Chapter 6 Higher Inductive Types
 
-```
-postulate
-  S¹ : Set
-  base : S¹
-  loop : base ≡ base
-```
+Using the approach from here: https://github.com/HoTT/HoTT-Agda/blob/master/old/Spaces/Circle.agda
 
 ## 6.2 Induction principles and dependent paths
 
@@ -50,4 +50,50 @@ record I-ind (P : I → Set) (b0 : P 0I) (b1 : P 1I) (s : b0 ≡[ P , seg ] b1)
     prop1 : f 0I ≡ b0
     prop2 : f 1I ≡ b1
     prop3 : apd f seg ≡ {! s  !}
+```
+
+## 6.4 Circles and sphere
+
+```
+private
+  data #S¹ : Set where
+    #base : #S¹
+
+S¹ : Set
+S¹ = #S¹
+
+base : S¹
+base = #base
+
+postulate
+  loop : base ≡ base
+
+S¹-rec : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
+S¹-rec b l #base = b
+
+postulate
+  S¹-rec-loop : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → apd (S¹-rec b l) loop ≡ l
+```
+
+### Lemma 6.4.1
+
+```
+lemma6∙4∙1 : loop ≢ refl
+lemma6∙4∙1 loop≡refl =
+  {!   !}
+  where
+    f : {A : Set} {x : A} {p : x ≡ x} → (S¹ → A)
+    f {A = A} {x = x} {p = p} s =
+      let p' = transportconst A loop x
+      in (S¹-rec x (p' ∙ p)) s
+    f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p
+    f-loop {x = x} = S¹-rec-loop x ?
+
+    goal : ⊥
+
+    goal2 : (A : Set l) (a : A) (p : a ≡ a) → isSet A 
+    goal = example3∙1∙9 (goal2 {!   !} {!   !} {!   !})
+
+    -- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl
+    goal2 A a p x y r s = {!   !}
 ```