wip exercise 3.1

src/HottBook/Chapter3.lagda.md

@@ -474,7 +474,7 @@ lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop prop2 ∣_∣ g
         what = gpx ∙ eqP
         prevResult = (lemma3∙9∙1 {P} Pprop) .snd .isequiv.g-id
       in
-      {!   !}
+      admit
       where
         postulate
           -- TODO: Finish this 
@@ -658,5 +658,8 @@ module lemma3∙11∙10 where
   i f x y = Σ.fst (f x y)
 
   ii : {A : Set} → isProp A → ((x y : A) → isContr (x ≡ y))
-  ii f x y = f x y , λ z → {!   !}
+  ii f x y = f x y , admit
+    where
+      postulate
+        admit : (z : x ≡ y) → f x y ≡ z
 ```

src/HottBook/Chapter3Exercises.lagda.md

@@ -16,17 +16,31 @@ exercise3∙1 : {A B : Set}
   → isSet A
   → isSet B
 exercise3∙1 {A} {B} equiv@(f , mkIsEquiv g g* h h*) isSetA xB yB pB qB =
-  let
-    xA = g xB
-    yA = g yB
-    pA : xA ≡ yA
-    pA = ap g pB
-    qA : xA ≡ yA
-    qA = ap g qB
-    eq = isSetA xA yA pA qA
-    idAB = axiom2∙10∙3.ua equiv
-    eqB = transport (λ S → {!   !}) idAB eq
-  in {!   !}
+  {!   !}
+  where
+    open axiom2∙10∙3
+    p : A ≡ B
+    p = ua equiv
+
+    lol = isSetA (g xB) (g yB) (ap g pB) (ap g qB)
+
+    lol2 : ap f (ap g pB) ≡ ap f (ap g qB)
+    lol2 = ap (ap f) lol
+
+    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 : ∀ {A B} {x y : B}
+    --   → (p : x ≡ y) → (f : A → B) → (g : B → A)
+    --   → ap (f ∘ g) ∼ id
+    -- lol4 refl f g x = {!   !}
+
 ```
 
 ### Exercise 3.5

src/HottBook/Chapter8.lagda.md

@@ -0,0 +1,17 @@
+<details>
+  <summary>Imports</summary>
+
+```
+module HottBook.Chapter8 where
+
+open import HottBook.Chapter1
+```
+
+</details>
+
+### Definition 8.0.1
+
+```
+π : (n : ℕ) → (A : Set) → (a : A) → Set
+-- π n A a = ∥ ? ∥₀
+```