diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index dc4c4e6..4574e1e 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -114,7 +114,7 @@ composite : {A B C : Set}
   → A → C
 composite f g x = g (f x)
 
-_∘_ : {A B C : Set}
+_∘_ : {l : Level} {A B C : Set l}
   → (g : B → C)
   → (f : A → B)
   → A → C
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index d0c5dc0..19c426a 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -205,7 +205,8 @@ Homotopy forms an equivalence relation:
 ### Definition 2.4.6
 
 ```
-record qinv {A B : Set} (f : A → B) : Set where
+record qinv {l : Level} {A B : Set l} (f : A → B) : Set l where
+  constructor mkQinv
   field
     g : B → A
     α : f ∘ g ∼ id
@@ -215,7 +216,7 @@ record qinv {A B : Set} (f : A → B) : Set where
 ### Example 2.4.7
 
 ```
-id-qinv : {A : Set} → qinv {A} id
+id-qinv : {l : Level} {A : Set l} → qinv {l} {A} id
 id-qinv = record
   { g = id
   ; α = λ _ → refl
@@ -226,7 +227,7 @@ id-qinv = record
 ### Definition 2.4.10
 
 ```
-record isequiv {A B : Set} (f : A → B) : Set where
+record isequiv {l : Level} {A B : Set l} (f : A → B) : Set l where
   constructor mkIsEquiv
   field
     g : B → A
@@ -236,7 +237,7 @@ record isequiv {A B : Set} (f : A → B) : Set where
 ```
 
 ```
-qinv-to-isequiv : {A B : Set}
+qinv-to-isequiv : {l : Level} {A B : Set l}
   → {f : A → B}
   → qinv f
   → isequiv f
@@ -251,8 +252,45 @@ qinv-to-isequiv q = record
 ### Definition 2.4.11
 
 ```
-_≃_ : (A B : Set) → Set
-A ≃ B = Σ[ f ∈ (A → B) ] isequiv f
+_≃_ : {l : Level} → (A B : Set l) → Set l
+A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
+```
+
+## 2.8 Σ-types
+
+### Theorem 2.7.2
+
+_Suppose that P : A → U is a type family over a type A and let w, w′ : ∑(x:A) P(x). Then there is an equivalence_
+
+```
+theorem2∙7∙2 : {l : Level} {A : Set l} {P : A → Set l}
+  → ((w @ (w1 , w2)) (w' @ (w'1 , w'2)) : Σ A P)
+  → (w ≡ w') ≃ Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2)
+theorem2∙7∙2 {l} {A} {P} (w @ (w1 , w2)) (w' @ (w'1 , w'2)) =
+  f , qinv-to-isequiv (mkQinv g forwards backwards)
+  where
+    f : (w ≡ w') → Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2)
+    f refl = refl , refl
+
+    g : Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2) → (w ≡ w') 
+    g (refl , refl) = refl
+
+    forwards : f ∘ g ∼ id
+    forwards (refl , refl) = refl
+
+    backwards : g ∘ f ∼ id
+    backwards refl = refl
+```
+
+### Corollary 2.7.3
+
+_For z : ∑(x:A) P(x), we have z = (pr1(z), pr2(z))._
+
+```
+corollary2∙7∙3 : {A : Set} {P : A → Set}
+  → (z @ (a , b) : Σ A P)
+  → z ≡ (a , b)
+corollary2∙7∙3 z = refl
 ```
 
 ## 2.8 The unit type