update

src/HottBook/Chapter1.lagda.md

@@ -200,7 +200,7 @@ _∘_ : {l1 l2 l3 : Level} {A : Set l1} {B : Set l2} {C : Set l3}
   → A → C
 _∘_ g f x = g (f x)
 
-composite-assoc : {A B C D : Set}
+composite-assoc : {A B C D : Set l}
   → (f : A → B)
   → (g : B → C)
   → (h : C → D)

src/HottBook/Chapter2.lagda.md

@@ -88,38 +88,38 @@ module lemma2∙1∙4 {l : Level} {A : Set l} where
 ### Theorem 2.1.6 (Eckmann-Hilton)
 
 ```
-module theorem2∙1∙6 where
-  Ω-type : (A : Set) → (a : A) → Set
-  Ω-type A a = refl {x = a} ≡ refl
+-- module theorem2∙1∙6 where
+--   Ω-type : (A : Set) → (a : A) → Set
+--   Ω-type A a = refl {x = a} ≡ refl
 
-  compose1 : {A : Set} {a : A} → fst (Ω (A , a)) → fst (Ω (A , a)) → fst (Ω (A , a))
-  compose1 x y = x ∙ y
+--   compose1 : {A : Set} {a : A} → fst (Ω (A , a)) → fst (Ω (A , a)) → fst (Ω (A , a))
+--   compose1 x y = x ∙ y
 
-  Ω² : {l : Level} → Set* l → Set* l
-  Ω² {l} = Ω[_] {l = l} 2
+--   Ω² : {l : Level} → Set* l → Set* l
+--   Ω² {l} = Ω[_] {l = l} 2
 
-  compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a))
-  compose2 x y = horiz x y
-    where
-      variable
-        A : Set l
-        a b c : A
-        p q : a ≡ b
-        r s : b ≡ c
-        α : p ≡ q
-        β : r ≡ s
+--   compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a))
+--   compose2 x y = horiz x y
+--     where
+--       variable
+--         A : Set l
+--         a b c : A
+--         p q : a ≡ b
+--         r s : b ≡ c
+--         α : p ≡ q
+--         β : r ≡ s
 
-      _∙ᵣ_ : p ≡ q → (r : b ≡ c) → p ∙ r ≡ q ∙ r
-      α ∙ᵣ refl = sym (lemma2∙1∙4.i1 _) ∙ α ∙ lemma2∙1∙4.i1 _
+--       _∙ᵣ_ : p ≡ q → (r : b ≡ c) → p ∙ r ≡ q ∙ r
+--       α ∙ᵣ refl = sym (lemma2∙1∙4.i1 _) ∙ α ∙ lemma2∙1∙4.i1 _
 
-      _∙ₗ_ : (q : a ≡ b) → r ≡ s → q ∙ r ≡ q ∙ s
-      refl ∙ₗ β = sym (lemma2∙1∙4.i2 _) ∙ β ∙ lemma2∙1∙4.i2 _
+--       _∙ₗ_ : (q : a ≡ b) → r ≡ s → q ∙ r ≡ q ∙ s
+--       refl ∙ₗ β = sym (lemma2∙1∙4.i2 _) ∙ β ∙ lemma2∙1∙4.i2 _
 
-      horiz : p ≡ q → r ≡ s → p ∙ r ≡ q ∙ s
-      horiz α β = (α ∙ᵣ _) ∙ (_ ∙ₗ β)
+--       horiz : p ≡ q → r ≡ s → p ∙ r ≡ q ∙ s
+--       horiz α β = (α ∙ᵣ _) ∙ (_ ∙ₗ β)
 
-  compose2-commutative : {l : Level} {A : Set l} {a : A} (x y : fst (Ω² (A , a))) → compose2 x y ≡ compose2 y x
-  compose2-commutative {l} {A} {a} x y = {! x !}
+--   compose2-commutative : {l : Level} {A : Set l} {a : A} (x y : fst (Ω² (A , a))) → compose2 x y ≡ compose2 y x
+--   compose2-commutative {l} {A} {a} x y = {!  !}
 ```
 
 ### Definition 2.1.7 (pointed type)
@@ -450,13 +450,13 @@ module lemma2∙4∙12 where
       e : isequiv id
       e = mkIsEquiv id (λ _ → refl) id (λ _ → refl)
 
-  sym-equiv : {A B : Set} → (f : A ≃ B) → B ≃ A
+  sym-equiv : {A B : Set l} → (f : A ≃ B) → B ≃ A
   sym-equiv {A} {B} (f , eqv) =
     let (mkQinv g α β) = isequiv-to-qinv eqv
     in g , qinv-to-isequiv (mkQinv f β α)
 
-  trans-equiv : {A B C : Set} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
-  trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) =
+  trans-equiv : {A B C : Set l} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
+  trans-equiv {l} {A} {B} {C} (f , f-eqv) (g , g-eqv) =
     let
       (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
       (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv
@@ -484,6 +484,27 @@ module lemma2∙4∙12 where
     in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)
 ```
 
+### ≃-Reasoning
+
+```
+module ≃-Reasoning where
+  infix 1 begin_
+  begin_ : {l : Level} {A B : Set l} → (A ≃ B) → (A ≃ B)
+  begin x = x
+
+  _≃⟨⟩_ : {l : Level} (A {B} : Set l) → A ≃ B → A ≃ B
+  _ ≃⟨⟩ x≃y = x≃y
+
+  infixr 2 _≃⟨⟩_ step-≃
+  step-≃ : {l : Level} (A {B C} : Set l) → B ≃ C → A ≃ B → A ≃ C
+  step-≃ _ y≃z x≃y = lemma2∙4∙12.trans-equiv x≃y y≃z
+  syntax step-≃ x y≃z x≃y = x ≃⟨ x≃y ⟩ y≃z
+
+  infix 3 _∎
+  _∎ : {l : Level} (A : Set l) → (A ≃ A)
+  A ∎ = lemma2∙4∙12.id-equiv A
+```
+
 ## 2.5 The higher groupoid structure of type formers
 
 ### Definition 2.5.1

src/HottBook/Chapter2Exercises.lagda.md

@@ -7,6 +7,10 @@ open import Agda.Primitive
 open import HottBook.Chapter1
 open import HottBook.Chapter2
 open import HottBook.Util
+
+private
+  variable
+    l l2 l3 : Level
 ```
 
 ## Exercise 2.1
@@ -171,9 +175,9 @@ TODO: Generalizing to dependent functions.
 ## Exercise 2.10
 
 ```
-exercise2∙10 : {A : Set} {B : A → Set} {C : Σ A B → Set}
+exercise2∙10 : (A : Set l) (B : A → Set l2) (C : Σ A B → Set l3)
   → (Σ A (λ x → Σ (B x) (λ y → C (x , y)))) ≃ Σ (Σ A B) C
-exercise2∙10 {A} {B} {C} = f , qinv-to-isequiv (mkQinv g f-g g-f)
+exercise2∙10 A B C = f , qinv-to-isequiv (mkQinv g f-g g-f)
   where
     f : (Σ A (λ x → Σ (B x) (λ y → C (x , y)))) → Σ (Σ A B) C
     f (x , (y , cxy)) = (x , y) , cxy

src/HottBook/Chapter3.lagda.md

@@ -437,11 +437,11 @@ module section3∙7 where
       → rec-trunc Bprop f (∣ a ∣) ≡ f a
     {-# REWRITE rec-trunc-1 #-}
 
-  ind-trunc : {A : Set} → {B : ∥ A ∥ → Set}
-    → ((x : ∥ A ∥) → isProp (B x))
-    → ((a : A) → B (∣ a ∣))
-    → (x : ∥ A ∥) → B x
-  ind-trunc f g x = rec-trunc (f x) (λ a → {! g x  !}) x
+  -- ind-trunc : {A : Set} → {B : ∥ A ∥ → Set}
+  --   → ((x : ∥ A ∥) → isProp (B x))
+  --   → ((a : A) → B (∣ a ∣))
+  --   → (x : ∥ A ∥) → B x
+  -- ind-trunc f g x = rec-trunc (f x) (λ a → {! g x  !}) x
 
 open section3∙7 public
 ```

src/HottBook/Chapter6.lagda.md

@@ -8,6 +8,7 @@ module HottBook.Chapter6 where
 
 open import HottBook.Chapter1
 open import HottBook.Chapter2
+open import HottBook.Chapter2Exercises
 open import HottBook.Chapter3
 open import HottBook.Chapter6Circle
 open import HottBook.CoreUtil
@@ -415,16 +416,41 @@ lemma6∙5∙3 A B* @ (B , b₀) = f , qinv-to-isequiv (mkQinv g forward {!   !}
 Susp* : {l : Level} → Set* l → Set* l
 Susp* (A , a₀) = Susp A , N
 
+Susp-universal-property : {A B : Set l}
+  → (Susp A → B) ≃ Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ))
+Susp-universal-property {l} {A} {B} = f , qinv-to-isequiv (mkQinv g forward backward)
+  where
+    f : (Susp A → B) → Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ))
+    f h = h N , h S , λ a → ap h (merid a)
+
+    g : Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ)) → (Susp A → B)
+    g (hn , hs , hm) sa = rec-Susp hn hs hm sa
+
+    forward : (f ∘ g) ∼ id
+    forward x = {! refl  !}
+
+    backward : (g ∘ f) ∼ id
+    backward x = {! refl  !}
+
+ap-equiv : {A B : Set l} → (F : Set l → Set l2) → (A ≃ B) → (F A ≃ F B)
+ap-equiv F (f , _) = (λ fa → {!   !}) , {!   !}
+
 lemma6∙5∙4 : {l : Level}
   → (A* @ (A , a₀) : Set* l)
   → (B* @ (B , b₀) : Set* l)
   → Map* {l = l} (Susp* A*) B* ≃ Map* A* (Ω B*)
-lemma6∙5∙4 A* B* = f , {!   !}
+lemma6∙5∙4 {l} A* @ (A , a₀) B* @ (B , b₀) = {!   !}
   where
-    f : Map* (Susp* A*) B* → Map* A* (Ω B*)
-    f (f' , p) = {!  f'' , ? !}
-      where
-        f'' : A* → Ω B*
+    open ≃-Reasoning
+    open lemma2∙4∙12
+    goal : Map* {l = l} (Susp* A*) B* ≃ Map* A* (Ω B*)
+    goal = begin
+      (Map* {l = l} (Susp* A*) B*) ≃⟨ id-equiv _ ⟩
+      (Σ (Susp A → B) (λ f → f N ≡ b₀)) ≃⟨ {! !} ⟩
+      (Σ (Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ))) (λ f → fst f ≡ b₀)) ≃⟨ sym-equiv (exercise2∙10 _ _ _) ⟩
+      (Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ) × (bₙ ≡ b₀))) ≃⟨ {!   !} ⟩
+      (Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ) × (bₙ ≡ b₀))) ≃⟨ {!   !} ⟩
+      (Map* A* (Ω B*)) ∎
 ```
 
 ## 6.6 Cell complexes

src/HottBook/Chapter6Exercises.lagda.md

@@ -2,4 +2,7 @@
 {-# OPTIONS --rewriting #-}
 
 module HottBook.Chapter6Exercises where
-```
+
+open import HottBook.Chapter6
+```
+