diff --git a/html/src/SUMMARY.md b/html/src/SUMMARY.md
index 3d38058..d817a58 100644
--- a/html/src/SUMMARY.md
+++ b/html/src/SUMMARY.md
@@ -10,6 +10,8 @@
- [Chapter 4](./generated/HottBook.Chapter4.md)
- [Chapter 5](./generated/HottBook.Chapter5.md)
- [Chapter 6](./generated/HottBook.Chapter6.md)
+- [Chapter 7](./generated/HottBook.Chapter7.md)
+- [Chapter 8](./generated/HottBook.Chapter8.md)
# HoTT Book (Cubical formulation)
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index bff06de..cb7a02d 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -96,19 +96,22 @@ pointed l = Σ (Set l) (λ A → A)
### Definition 2.1.8 (loop space)
```
-Ω : {l : Level} → pointed l → pointed l
-Ω (A , a) = (a ≡ a) , refl
+Ω : {l : Level} → pointed l → Set l
+Ω (A , a) = a ≡ a
```
### Theorem 2.1.6 (Eckmann-Hilton)
```
module theorem2∙1∙6 where
- Ω² : {l : Level} → pointed l → pointed l
- Ω² p = Ω (Ω p)
+ Ω² : {l : Level} → pointed l → Set l
+ Ω² p = Ω (Ω p , refl)
- -- compose : {l : Level} {p : pointed {l}} → (Ω² p) × (Ω² p) → Ω² p
- -- compose a b = ?
+ compose : {l : Level} {p : pointed l} → (Ω² p) × (Ω² p) → Ω² p
+ compose (a , b) = a ∙ b
+
+ -- commute : {l : Level} {p : pointed l} → (α β : Ω² p) → α ∙ β ≡ β ∙ α
+ -- commute {l} {p @ (A , a₀)} α β = {! !}
```
## 2.2 Functions are functors
@@ -312,6 +315,7 @@ lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} refl =
-- → H (f x) ≡ ap f (H x)
-- corollary2∙4∙4 {A} {f} {H} x =
-- let g p = H x in
+-- -- let naturality = lemma2∙4∙3 H x in
-- {! !}
```
@@ -1043,4 +1047,31 @@ theorem2∙15∙5 {X = X} {A = A} {B = B} = qinv-to-isequiv (mkQinv g forward ba
backward : (f : (x : X) → A x × B x) → g (equation2∙15∙4 f) ≡ f
backward f = funext λ x → refl
where open axiom2∙9∙3
-```
\ No newline at end of file
+```
+
+### Equation 2.15.6
+
+```
+equation2∙15∙6 : {X : Set} {A : X → Set} {P : (x : X) → A x → Set}
+ → ((x : X) → Σ (A x) (P x))
+ → Σ ((x : X) → A x) (λ g → (x : X) → P x (g x))
+equation2∙15∙6 f = (λ x → fst (f x)) , λ x → snd (f x)
+```
+
+### Theorem 2.15.7
+
+```
+theorem2∙15∙7 : {X : Set} {A : X → Set} {P : (x : X) → A x → Set} → isequiv (equation2∙15∙6 {X = X} {A = A} {P = P})
+theorem2∙15∙7 {X} {A} {P} = qinv-to-isequiv (mkQinv g forward backward)
+ where
+ open axiom2∙9∙3
+
+ g : Σ ((x : X) → A x) (λ g → (x : X) → P x (g x)) → (x : X) → Σ (A x) (P x)
+ g (f1 , f2) x = f1 x , f2 x
+
+ forward : (equation2∙15∙6 ∘ g) ∼ id
+ forward (f1 , f2) = Σ-≡ (refl , refl)
+
+ backward : (g ∘ equation2∙15∙6) ∼ id
+ backward f = funext λ x → refl
+```
\ No newline at end of file
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index 1a1ab29..2952b22 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -357,7 +357,6 @@ lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward)
goal2 : (y : 𝟚) → {! !} ∙ refl ∙ {! !} ≡ merid true
goal y = {! !}
-
```
### Definition 6.5.2