diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 12753e6..cd8c014 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -454,7 +454,7 @@ A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
 
 ```
 module lemma2∙4∙12 where
-  id-equiv : (A : Set) → A ≃ A
+  id-equiv : {l : Level} → (A : Set l) → A ≃ A
   id-equiv A = id , e
     where
       e : isequiv id
@@ -545,26 +545,46 @@ definition2∙6∙1 p = ap Σ.fst p , ap Σ.snd p
 ### Theorem 2.6.2
 
 ```
--- theorem2∙6∙2 : {A B : Set} (x y : A × B)
---   → isequiv (definition2∙6∙1 {A} {B} {x} {y})
--- theorem2∙6∙2 {A} {B} x y = qinv-to-isequiv (mkQinv g {!   !} {!   !})
---   where
---     g : (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) → x ≡ y
---     g p =
---       let (p1 , p2) = p in
---       J
---         (λ x3 y3 p3 → (x4 y4 : B) → (p2 : x4 ≡ y4) → (x3 , x4) ≡ (y3 , y4))
---         (λ x1 x4 y4 p2 → J (λ x4 y4 p2 → (x1 , x4) ≡ (x1 , y4)) (λ _ → refl) x4 y4 p2)
---         (Σ.fst x) (Σ.fst y) p1 (Σ.snd x) (Σ.snd y) p2
+module theorem2∙6∙2 where
+  pair-≡ : {A B : Set} {x y : A × B} → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) → x ≡ y
+  pair-≡ (refl , refl) = refl
 
---     backward : (definition2∙6∙1 ∘ g) ∼ id
---     backward x = {!   !}
+  theorem2∙6∙2 : {A B : Set} {x y : A × B}
+    → isequiv (definition2∙6∙1 {A} {B} {x} {y})
+  theorem2∙6∙2 {A} {B} {x} {y} = qinv-to-isequiv (mkQinv pair-≡ backward forward)
+    where
+      backward : (definition2∙6∙1 ∘ pair-≡) ∼ id
+      backward (refl , refl) = refl
+
+      forward : (pair-≡ ∘ definition2∙6∙1) ∼ id
+      forward refl = refl
+
+open theorem2∙6∙2 using (pair-≡)
+```
+
+### Theorem 2.6.4
+
+```
+theorem2∙6∙4 : {Z : Set} {A B : Z → Set} {z w : Z}
+  → (p : z ≡ w) 
+  → (x : A z × B z)
+  → transport (λ z → A z × B z) p x ≡ (transport A p (Σ.fst x) , transport B p (Σ.snd x))
+theorem2∙6∙4 {Z} {A} {B} {z} {w} refl x = refl
 ```
 
 ### Theorem 2.6.5
 
 ```
-
+theorem2∙6∙5 : {A A' B B' : Set} {g : A → A'} {h : B → B'} 
+  → (x y : A × B)
+  → (p : Σ.fst x ≡ Σ.fst y)
+  → (q : Σ.snd x ≡ Σ.snd y)
+  → let
+      f : A × B → A' × B'
+      f z = (g (Σ.fst z) , h (Σ.snd z)) 
+    in
+    ap f (pair-≡ (p , q)) ≡ pair-≡ (ap g p , ap h q)
+theorem2∙6∙5 x y refl refl = refl
 ```
 
 ## 2.7 Σ-types
@@ -612,7 +632,7 @@ corollary2∙7∙3 z = refl
 --   → {x y : A}
 --   → (p : x ≡ y)
 --   → (u z : Σ (P x) (λ u → Q (x , u)))
---   → {!   !}
+--   → transport {!  P !} p (u , z) ≡ (transport {!  P !} p u , transport {!   !} (pair-≡ (p , refl)) z)
 ```
 
 ## 2.8 The unit type
@@ -700,18 +720,18 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where
   hat B (fst , snd) = B fst snd
 
   --- I have no idea where this goes but this definitely needs to exist
-  pair-≡ : {A : Set} {B : A → Set} {a1 a2 : A} {b1 : B a1} {b2 : B a2}
+  pair-≡-d : {A : Set} {B : A → Set} {a1 a2 : A} {b1 : B a1} {b2 : B a2}
     → (p : a1 ≡ a2) → (transport B p b1 ≡ b2) → (a1 , b1) ≡ (a2 , b2)
-  pair-≡ refl refl = refl
+  pair-≡-d refl refl = refl
 
   equation2∙9∙5 : (A : X → Set)
     → (B : (x : X) → A x → Set)
     → (f : (a : A x1) → B x1 a)
     → (p : x1 ≡ x2)
     → (a : A x2)
-    → transport (Π A B) p f a ≡ transport (hat B) (sym (pair-≡ (sym p) refl)) (f (transport A (sym p) a))
+    → transport (Π A B) p f a ≡ transport (hat B) (sym (pair-≡-d (sym p) refl)) (f (transport A (sym p) a))
   equation2∙9∙5 A B f p a =
-    J (λ x1' x2' p' → (f' : (a : A x1') → B x1' a) → (a' : A x2') → transport (Π A B) p' f' a' ≡ transport (hat B) (sym (pair-≡ (sym p') refl)) (f' (transport A (sym p') a')))
+    J (λ x1' x2' p' → (f' : (a : A x1') → B x1' a) → (a' : A x2') → transport (Π A B) p' f' a' ≡ transport (hat B) (sym (pair-≡-d (sym p') refl)) (f' (transport A (sym p') a')))
       (λ x' f' a' → refl) x1 x2 p f a
 ```
 
@@ -740,13 +760,14 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where
 idtoeqv : {l : Level} {A B : Set l}
   → (A ≡ B)
   → (A ≃ B)
-idtoeqv {l} {A} {B} p = J C c A B p
-  where
-    C : (x y : Set l) (p : x ≡ y) → Set l
-    C x y p = x ≃ y
+idtoeqv {l} {A} {B} refl = lemma2∙4∙12.id-equiv A
+-- idtoeqv {l} {A} {B} p = J C c A B p
+  -- where
+  --   C : (x y : Set l) (p : x ≡ y) → Set l
+  --   C x y p = x ≃ y
 
-    c : (x : Set l) → C x x refl
-    c x = id , qinv-to-isequiv id-qinv
+  --   c : (x : Set l) → C x x refl
+  --   c x = id , qinv-to-isequiv id-qinv
 ```
 
 ### Axiom 2.10.3 (Univalence)
@@ -1018,4 +1039,20 @@ theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl)
   where
     g : (X → A) × (X → B) → (X → A × B)
     g (f1 , f2) = λ x → (f1 x , f2 x)
-```     
\ No newline at end of file
+```
+
+### Equation 2.15.4
+
+```
+equation2∙15∙4 : {X : Set} {A B : X → Set}
+  → ((x : X) → A x × B x)
+  → ((x : X) → A x) × ((x : X) → B x)
+equation2∙15∙4 f = ((λ x → Σ.fst (f x)) , λ x → Σ.snd (f x))
+```
+
+### Theorem 2.15.5
+
+```
+-- theorem2∙15∙5 : isequiv equation2∙15∙4
+-- theorem2∙15∙5 = qinv-to-isequiv (mkQinv {!   !} {!   !} {!   !})
+```
\ No newline at end of file
diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 4ab398d..a8bf905 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -63,9 +63,9 @@ $A$, simultaneously with the type of boundaries for such paths._
 [6]: https://git.mzhang.io/school/type-theory/issues/6
 
 ```
-data n-dimensional-path {A : Set} : (n : ℕ) → Set where
-  z : (x y : A) → x ≡ y → n-dimensional-path zero
-  s : (n : ℕ) → (d : n-dimensional-path {A} n) → n-dimensional-path (suc n)
+-- data n-dimensional-path {A : Set} : (n : ℕ) → Set where
+--   z : (x y : A) → x ≡ y → n-dimensional-path zero
+--   s : (n : ℕ) → (d : n-dimensional-path {A} n) → n-dimensional-path (suc n)
 -- n-dimensional-path {A} zero = (x y : A) → x ≡ y
 -- n-dimensional-path {A} (suc n) = {!   !}
 ```
@@ -100,6 +100,38 @@ module exercise2∙5 {A B : Set} {x y : A} {p : x ≡ y} {f : A → B} where
     in z3 ∙ z2 ∙ z4
 ```
 
+## Exercise 2.6
+
+```
+exercise2∙6 : {l : Level} {A : Set l} {x y z : A}
+  → (p : x ≡ y)
+  → isequiv (λ (q : y ≡ z) → p ∙ q)
+exercise2∙6 {l} {A} {x} {y} {z} p = qinv-to-isequiv (mkQinv g forward backward)
+  where
+    f : y ≡ z → x ≡ z
+    f q = p ∙ q
+
+    g : x ≡ z → y ≡ z
+    g q = sym p ∙ q
+
+    forward : (f ∘ g) ∼ id
+    forward q = let
+      z1 = lemma2∙1∙4.ii2 p
+      z2 = ap (λ r → r ∙ q) z1
+      z3 = lemma2∙1∙4.iv p (sym p) q
+      z4 = sym (lemma2∙1∙4.i2 q)
+      in z3 ∙ z2 ∙ z4
+
+    backward : (g ∘ f) ∼ id
+    backward q = let
+      z1 = lemma2∙1∙4.ii1 p
+      z2 = ap (λ r → r ∙ q) z1
+      z3 = lemma2∙1∙4.iv (sym p) p q
+      z4 = sym (lemma2∙1∙4.i2 q)
+      in z3 ∙ z2 ∙ z4
+
+```
+
 ## Exercise 2.9
 
 Prove that coproducts have the expected universal property,
@@ -134,6 +166,10 @@ TODO: Generalizing to dependent functions.
 
 ## Exercise 2.10
 
+```
+
+```
+
 ## Exercise 2.13
 
 _Show that $(2 \simeq 2) \simeq 2$._
@@ -227,3 +263,54 @@ exercise2∙13 = f , equiv
     equiv : isequiv f
     equiv = mkIsEquiv g f∘g∼id g g∘f∼id
 ```
+
+## Exercise 2.16
+
+```
+module exercise2∙16 where
+  postulate
+    notFunext : {l1 l2 : Level} (A : Set l1) → (B : A → Set l2) → (f g : (x : A) → B x) → (f ∼ g) → (f ≡ g)
+
+  realFunext : {l : Level} {A B : Set l} → {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
+  realFunext {l} {A} {B} {f} {g} p = notFunext A {! B   !} {!   !} {!   !} {!   !}
+```
+
+## Exercise 2.17
+
+```
+module exercise2∙17 where
+  open axiom2∙10∙3 hiding (forward; backward)
+  statement = {A A' B B' : Set} → A ≃ A' → B ≃ B' → (A × B) ≃ (A' × B')
+
+  --- I have no idea where this goes but this definitely needs to exist
+  pair-≡ : {l : Level} {A A' B B' : Set l}
+    → (p : A ≡ A') → (B ≡ B') → (A × B) ≡ (A' × B')
+  pair-≡ refl refl = refl
+
+  -- Without univalence
+  i : statement
+  i {A} {A'} {B} {B'} (A-eqv @ (Af , A-isequiv)) (B-eqv @ (Bf , B-isequiv)) =
+    f , qinv-to-isequiv (mkQinv g {!   !} {!   !})
+    where 
+      f : (A × B) → (A' × B')
+      f (a , b) = Af a , Bf b
+
+      g : (A' × B') → (A × B)
+      g (a' , b') = (isequiv.g A-isequiv) a' , (isequiv.g B-isequiv) b'
+
+      backward : (f ∘ g) ∼ id
+      backward x = {!   !}
+
+      forward : (g ∘ f) ∼ id
+      forward x = {!   !}
+
+  -- With univalence
+  ii : statement
+  ii {A} {A'} {B} {B'} A-eqv B-eqv =
+    let
+      A-id = ua A-eqv
+      B-id = ua B-eqv
+
+      combined-id = pair-≡ A-id B-id
+    in idtoeqv combined-id
+```
\ No newline at end of file