diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index cb7a02d..db399be 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -11,6 +11,7 @@ open import HottBook.Chapter1
 open import HottBook.Chapter1Util
 open import HottBook.Chapter2Lemma221 public
 open import HottBook.Chapter2Lemma231 public
+open import HottBook.Chapter2Definition217 public
 
 private
   variable
@@ -84,36 +85,34 @@ module lemma2∙1∙4 {l : Level} {A : Set l} where
   iv {x} {y} {z} {w} refl refl refl = refl
 ```
 
-### Definition 2.1.7 (pointed type)
-
-This comes first, since it is needed to define Theorem 2.1.6.
-
-```
-pointed : (l : Level) → Set (lsuc l)
-pointed l = Σ (Set l) (λ A → A)
-```
-
-### Definition 2.1.8 (loop space)
-
-```
-Ω : {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 → Set l
-  Ω² p = Ω (Ω p , refl)
+  Ω-type : (A : Set) → (a : A) → Set
+  Ω-type A a = refl {x = a} ≡ refl
 
-  compose : {l : Level} {p : pointed l} → (Ω² p) × (Ω² p) → Ω² p
-  compose (a , b) = a ∙ b
+  compose1 : {A : Set} {a : A} → fst (Ω (A , a)) → fst (Ω (A , a)) → fst (Ω (A , a))
+  compose1 x y = x ∙ y
 
-  -- commute : {l : Level} {p : pointed l} → (α β : Ω² p) → α ∙ β ≡ β ∙ α
-  -- commute {l} {p @ (A , a₀)} α β = {!  !}
+  Ω² : {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 = x ∙ y
+
+  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)
+
+{{#include HottBook.Chapter2Definition217.md:pointedtype}}
+
+### Definition 2.1.8 (loop space)
+
+{{#include HottBook.Chapter2Definition217.md:loopspace}}
+
 ## 2.2 Functions are functors
 
 ### Lemma 2.2.1
diff --git a/src/HottBook/Chapter2Definition217.lagda.md b/src/HottBook/Chapter2Definition217.lagda.md
new file mode 100644
index 0000000..e0d1b55
--- /dev/null
+++ b/src/HottBook/Chapter2Definition217.lagda.md
@@ -0,0 +1,30 @@
+```
+{-# OPTIONS --rewriting #-}
+
+module HottBook.Chapter2Definition217 where
+
+open import Agda.Primitive
+open import HottBook.Chapter1
+```
+
+[//]: <> (ANCHOR: pointedtype)
+
+```
+Set* : (l : Level) → Set (lsuc l)
+Set* l = Σ (Set l) (λ A → A)
+```
+
+[//]: <> (ANCHOR_END: pointedtype)
+
+[//]: <> (ANCHOR: loopspace)
+
+```
+Ω : {l : Level} → Set* l → Set* l
+Ω (A , a) = (a ≡ a) , refl
+
+Ω[_] : {l : Level} → ℕ → Set* l → Set* l
+Ω[ zero ] (A , a) = (A , a)
+Ω[ suc n ] (A , a) = Ω[ n ] (Ω (A , a))
+```
+
+[//]: <> (ANCHOR_END: loopspace)
\ No newline at end of file
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index 2952b22..35264af 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -300,10 +300,10 @@ module Suspension where
       A : Set l
 
   postulate
-    Susp : Set → Set
+    Susp : Set l → Set l
     N : Susp A
     S : Susp A
-    merid : A → (N {A} ≡ S {A})
+    merid : A → (N {A = A} ≡ S {A = A})
 
     rec-Susp : {B : Set l} → (n s : B) → (m : A → n ≡ s) → Susp A → B
     rec-Susp-N : {B : Set l} → (n s : B) → (m : A → n ≡ s) → rec-Susp n s m N ≡ n
@@ -371,7 +371,7 @@ module definition6∙5∙2 where
 ### Lemma 6.5.3
 
 ```
-Map* : {l : Level} → (A B : pointed l) → Set l
+Map* : {l : Level} → (A B : Set* l) → Set l
 Map* (A , a₀) (B , b₀) = Σ (A → B) (λ f → f a₀ ≡ b₀)
 ```
 
@@ -379,13 +379,13 @@ Adjoining a disjoint basepoint
 
 ```
 module lol where
-  _₊ : {l : Level} → Set l → pointed l
+  _₊ : {l : Level} → Set l → Set* l
   A ₊ = A + Lift 𝟙 , inr (lift tt)
 ```
 
 ```
 open lol
-lemma6∙5∙3 : {l : Level} (A : Set l) → (B* @ (B , b₀) : pointed l)
+lemma6∙5∙3 : {l : Level} (A : Set l) → (B* @ (B , b₀) : Set* l)
   → (Map* (A ₊) B*) ≃ (A → B)
 lemma6∙5∙3 A B* @ (B , b₀) = f , qinv-to-isequiv (mkQinv g forward {!   !})
   where
@@ -409,6 +409,24 @@ lemma6∙5∙3 A B* @ (B , b₀) = f , qinv-to-isequiv (mkQinv g forward {!   !}
       -- g (f' x) gives us b₀
 ```
 
+### Lemma 6.5.4
+
+```
+Susp* : {l : Level} → Set* l → Set* l
+Susp* (A , a₀) = Susp A , N
+
+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 , {!   !}
+  where
+    f : Map* (Susp* A*) B* → Map* A* (Ω B*)
+    f (f' , p) = {!  f'' , ? !}
+      where
+        f'' : A* → Ω B*
+```
+
 ## 6.6 Cell complexes
 
 ```