updates

src/HottBook/Chapter1.lagda.md

@@ -6,7 +6,7 @@
 
 module HottBook.Chapter1 where
 
-open import Agda.Primitive public
+open import Agda.Primitive hiding (Prop) public
 open import HottBook.CoreUtil
 
 private

src/HottBook/Chapter2.lagda.md

@@ -754,7 +754,8 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where
 ### Lemma 2.9.6
 
 ```
--- module lemma2∙9∙6 {X : Set} {A B : X → Set} {x y : X} where
+-- module lemma2∙9∙6 where
+
 --   P : (x : X) → Set
 --   P x = A x → B x
 

src/HottBook/Chapter3.lagda.md

@@ -350,6 +350,20 @@ module lemma3∙3∙5 where
 
 ## 3.4 Classical vs. intuitionistic logic
 
+### Definition 3.4.1 (LEM)
+
+```
+LEM : {l : Level} → Set (lsuc l)
+LEM {l} = (A : Set l) → (isProp A) → (A + (¬ A))
+```
+
+### Definition 3.4.2 (Double negation)
+
+```
+double-negation : {l : Level} → Set (lsuc l)
+double-negation {l} = (A : Set l) → isProp A → (¬ ¬ A → A)
+```
+
 ### Definition 3.4.3
 
 ```
@@ -361,7 +375,7 @@ module definition3∙4∙3 where
     proof : (a : A) → (B a + (¬ (B a))) → decidable-family B
 
   data decidable-equality (A : Set) : Set where
-    proof : (a b : A) → ((a ≡ b) + (¬ a ≡ b)) → decidable-equality A
+    proof : ((a b : A) → (a ≡ b) + (¬ a ≡ b)) → decidable-equality A
 ```
 
 ## 3.5 Subsets and propositional resizing

src/HottBook/Chapter3Exercises.lagda.md

@@ -4,8 +4,10 @@
 module HottBook.Chapter3Exercises where
 
 open import HottBook.Chapter1
+open import HottBook.Chapter1Util
 open import HottBook.Chapter2
 open import HottBook.Chapter3
+open import HottBook.CoreUtil
 ```
 
 ### Exercise 3.1
@@ -59,17 +61,144 @@ exercise3∙1 {A} {B} equiv@(f , mkIsEquiv g g* h h*) isSetA xB yB pB qB =
 
 ```
 
+### Exercise 3.2
+
+```
+exercise3∙2 : {A B : Set}
+  → isSet A
+  → isSet B
+  → isSet (A + B)
+exercise3∙2 A-set B-set (inl x) (inl .x) refl q = let z = A-set x x refl {!   !} in {!   !}
+exercise3∙2 A-set B-set (inr x) (inr y) p q = {!   !}
+```
+
+### Exercise 3.4
+
+```
+module exercise3∙4 {A : Set} where
+  open axiom2∙9∙3
+
+  forwards : isContr (A → A) → isProp A
+  forwards A→A-contr @ (center , proof) x y = happly p x
+    where
+      f = λ _ → x
+      g = λ _ → y
+
+      p : f ≡ g
+      p = sym (proof f) ∙ proof g
+
+  backwards : isProp A → isContr (A → A)
+  backwards A-prop = id , λ f → funext λ x → A-prop x (f x)
+```
+
 ### Exercise 3.5
 
 ```
-exercise3∙5 : ∀ {A} → isProp A ≃ ((x : A) → isContr A)
-exercise3∙5 {A} = {!  f , ? !}
+exercise3∙5 : ∀ {l} {A : Set l} → isProp A ≃ ((x : A) → isContr A)
+exercise3∙5 {A = A} = f , qinv-to-isequiv (mkQinv g forward backward)
   where
+    open axiom2∙9∙3
+
     f : isProp A → ((x : A) → isContr A)
-    f AisProp x = x , λ y → AisProp x y
+    f A-prop x = x , λ y → A-prop x y
 
     g : ((x : A) → isContr A) → isProp A
-    g func x y = {!   !}
+    g func x y = p1 ∙ p ∙ p2
+      where
+        center1 : A
+        center1 = fst (func x)
+
+        proof1 : (a : A) → center1 ≡ a
+        proof1 = snd (func x)
+
+        center2 : A
+        center2 = fst (func y)
+
+        proof2 : (a : A) → center2 ≡ a
+        proof2 = snd (func y)
+
+        p : center1 ≡ center2
+        p = proof1 center2
+
+        p1 : x ≡ center1
+        p1 = sym (proof1 x)
+
+        p2 : center2 ≡ y
+        p2 = proof2 y
+
+    forward : (f ∘ g) ∼ id
+    forward h = funext λ x → Σ-≡ (p1 , p2)
+      where
+        p1 : {x : A} → fst ((f ∘ g) h x) ≡ fst (id h x)
+        p1 {x} = sym (snd (h x) (fst ((f ∘ g) h x)))
+
+        p2 : {x : A} → transport (λ a → (x₁ : A) → a ≡ x₁) p1 (snd ((f ∘ g) h x)) ≡ snd (id h x)
+        p2 {x} = funext (helper x)
+          where
+            helper2 : (x y : A) 
+              → (res : fst (h x) ≡ y)
+              → (eq : snd (h x) y ≡ res)
+              → transport (λ a → (z : A) → a ≡ z) (sym (snd (h x) x))
+                (λ y₁ → trans (sym (snd (h x) x)) (trans (snd (h x) (fst (h y₁))) (snd (h y₁) y₁)))
+                y ≡ res
+            helper2 x .(fst (h x)) refl eq = {!   !}
+
+            helper : (x y : A) → transport (λ a → (z : A) → a ≡ z) p1 (snd ((f ∘ g) h x)) y ≡ snd (h x) y
+            helper x y with res ← snd (h x) y in eq = {!   !}
+
+
+    backward : (g ∘ f) ∼ id
+    backward A-prop = funext λ x → funext λ y → (goal x y)
+      where
+        open ≡-Reasoning
+
+        helper : {x y : A} {res : x ≡ y} → (sym (A-prop x x)) ∙ (trans res (A-prop y y)) ≡ res
+        helper {x} {res = refl} =
+          sym (A-prop x x) ∙ (refl ∙ (A-prop x x)) ≡⟨ ap (sym (A-prop x x) ∙_) (sym (lemma2∙1∙4.i2 (A-prop x x))) ⟩
+          sym (A-prop x x) ∙ (A-prop x x) ≡⟨ lemma2∙1∙4.ii1 (A-prop x x) ⟩
+          refl ∎
+
+        goal : (x y : A) → (g ∘ f) A-prop x y ≡ id A-prop x y
+        goal x y with res ← A-prop x y in eq = helper
+```
+
+### Exercise 3.6
+
+```
+exercise3∙6 : {A : Set} → isProp A → isProp (A + (¬ A))
+exercise3∙6 A-prop (inl x) (inl y) = ap inl (A-prop x y)
+exercise3∙6 A-prop (inr x) (inl y) = rec-⊥ (x y)
+exercise3∙6 A-prop (inl x) (inr y) = rec-⊥ (y x)
+exercise3∙6 A-prop (inr x) (inr y) = ap inr (funext λ a → rec-⊥ (x a)) where open axiom2∙9∙3
+```
+
+### Exercise 3.9
+
+```
+Prop : {l : Level} → Set (lsuc l)
+Prop {l} = Σ (Set l) isProp
+
+exercise3∙9 : {l : Level} → LEM {l} → Prop {l} ≃ 𝟚
+exercise3∙9 {l} lem = f , qinv-to-isequiv (mkQinv g forward {!   !})
+  where
+    open ≡-Reasoning
+    open Lift
+
+    lemMap : {A : Set l} → (A + (¬ A)) → 𝟚
+    lemMap {A} (inl x) = true
+    lemMap {A} (inr x) = false
+
+    f : Prop {l} → 𝟚
+    f (A , A-prop) = lemMap (lem A A-prop)
+
+    g : 𝟚 → Prop {l}
+    g _ = Lift 𝟙 , λ x y → ap lift (𝟙-isProp (lower x) (lower y))
+
+    forward : (f ∘ g) ∼ id
+    forward p =
+      (f ∘ g) true ≡⟨⟩
+      lemMap (lem (Lift 𝟙) (λ x y → ap lift (𝟙-isProp (lower x) (lower y)))) ≡⟨ {!  refl !} ⟩
+      p ∎
 ```
 
 ### Exercise 3.19
@@ -85,4 +214,11 @@ exercise3∙19 P Pdecidable trunc = {!   !}
 
 ```
 exercise3∙20 = lemma3∙11∙9.ii
+```
+
+### Exercise 3.21
+
+```
+exercise3∙21 : {P : Set} → isProp P ≃ (P ≃ ∥ P ∥)
+exercise3∙21 {P} = {!   !} , {!   !}
 ```

src/HottBook/Chapter7.lagda.md

@@ -39,4 +39,117 @@ theorem7∙1∙4 : {X Y : Set}
   → (f : X → Y) → (n : ℕ') → is n type X → is n type Y
 theorem7∙1∙4 {X} {Y} f negtwo q = f (fst q) , λ y → {!   !}
 theorem7∙1∙4 {X} {Y} f (suc n) q = {!   !}
+```
+
+### Theorem 7.2.2
+
+```
+module lemma2∙9∙6 where
+  stmt : {X : Set} {A B : X → Set} {x y : X}
+    → (p : x ≡ y)
+    → (f : A x → B x)
+    → (g : A y → B y)
+    → (transport (λ z → A z → B z) p f ≡ g) ≃ ((a : A x) → (transport (λ z → B z) p (f a)) ≡ g (transport (λ z → A z) p a))
+  stmt {X} {A} {B} {x} {.x} refl f g = f' , qinv-to-isequiv (mkQinv g' {!   !} {!   !})
+    where
+      open axiom2∙9∙3
+
+      f' : f ≡ g → (a : A x) → f a ≡ g a
+      f' p = happly p
+
+      g' : ((a : A x) → f a ≡ g a) → f ≡ g
+      g' h = funext h
+
+Prop : {l : Level} → Set (lsuc l)
+Prop {l} = Σ (Set l) isProp
+
+theorem7∙2∙2 : {l : Level} {X : Set l} → {R : X → X → Prop {l = l}}
+  → (ρ : (x : X) → R x x)
+  → (f : (x y : X) → R x y → x ≡ y) → isSet X
+theorem7∙2∙2 {X} {R} ρ f = {!  !}
+  where
+    variable
+      x : X
+      p : x ≡ x
+      r : R x x
+
+    apdfp : transport (λ x → x ≡ x) p (f x x (ρ x)) ≡ f x x (ρ x)
+    apdfp {p = p} = apd (λ x → f x x (ρ x)) p
+
+    step2 : {x : X} {p : x ≡ x}
+      → (r : R x x)
+      → transport (λ z → z ≡ z) p (f x x r) ≡ f x x (transport (λ z → R z z) p r)
+    step2 {x} {p} r =
+      let
+        f' = f x x
+        helper = lemma2∙9∙6.stmt {A = λ z → R z z} p f' f'
+      in (fst helper) refl (ρ x)
+```
+
+### Lemma 7.2.4
+
+```
+lemma7∙2∙4 : {A : Set} → (A + (¬ A)) → (¬ ¬ A → A)
+lemma7∙2∙4 {A} (inl x) ¬¬A = x
+lemma7∙2∙4 {A} (inr x) ¬¬A = rec-⊥ (¬¬A x)
+```
+
+### Corollary 7.2.3
+
+```
+theorem7∙2∙3 : {X : Set} → (x y : X) → ¬ ¬ (x ≡ y) → isSet X
+theorem7∙2∙3 x y u =
+  let what = lemma7∙2∙4 {!   !} u
+  in {!   !}
+```
+
+### Theorem 7.2.5
+
+```
+theorem7∙2∙5 : {X : Set} → definition3∙4∙3.decidable-equality X → isSet X
+theorem7∙2∙5 {X} (definition3∙4∙3.proof f) x y p q with prf ← f x y in eq = helper prf eq
+  where
+    helper : (prf : (x ≡ y) + (x ≡ y → ⊥)) → (f x y ≡ prf) → p ≡ q
+    helper (inl z) eq = theorem7∙2∙3 x y (λ n → n p) x y p q
+    helper (inr g) eq = rec-⊥ (g p)
+
+hedberg : {X : Set} → definition3∙4∙3.decidable-equality X → isSet X
+hedberg {X} (definition3∙4∙3.proof d) x y p q = {!   !}
+  where
+    open ≡-Reasoning
+    -- d : (a b : X) → (a ≡ b) + (¬ a ≡ b)
+
+    res : (x ≡ y) + (¬ x ≡ y)
+    res = d x y
+
+    r : (x y : X) → x ≡ y → x ≡ y
+    r x y p with res ← d x y in eq = helper res
+      where
+        helper : (x ≡ y) + (x ≡ y → ⊥) → x ≡ y
+        helper (inl x) = x
+        helper (inr x) = rec-⊥ (x p)
+
+    r-constant : (x y : X) → (p q : x ≡ y) → r x y p ≡ r x y q
+
+    s : (x y : X) → x ≡ y → x ≡ y
+    s x y p = sym (r x x refl) ∙ r x y p
+
+    lemma1 : {x y : X} (p : x ≡ y) → s x y p ≡ p
+    lemma1 {x} refl =
+      s x x refl ≡⟨⟩
+      sym (r x x refl) ∙ r x x refl ≡⟨ lemma2∙1∙4.ii1 (r x x refl) ⟩
+      refl ∎
+
+    lemma2 : {x y : X} (p q : x ≡ y) → s x y p ≡ s x y q
+    lemma2 {x} {y} p q =
+      s x y p ≡⟨⟩
+      sym (r x x refl) ∙ r x y p ≡⟨ ap (sym (r x x refl) ∙_) (r-constant x y p q) ⟩
+      sym (r x x refl) ∙ r x y q ≡⟨⟩
+      s x y q ∎
+    
+    -- general-lemma refl f = lemma2∙1∙4.i1 (f refl)
+
+    -- helper : (prf : (x ≡ y) + (x ≡ y → ⊥)) → (f x y ≡ prf) → p ≡ q
+    -- helper (inl z) eq = {!   !}
+    -- helper (inr g) eq = rec-⊥ (g p)
 ```