diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 5e76081..9209779 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -6,7 +6,7 @@ module HottBook.Chapter2 where
 
 open import Agda.Primitive
 open import HottBook.Chapter1
-open import HottBook.Chapter2Lemma221
+open import HottBook.Chapter2Lemma221 public
 open import HottBook.Util
 ```
 
@@ -738,45 +738,67 @@ open axiom2∙10∙3
 ### Theorem 2.11.1
 
 ```
-theorem2∙11∙1 : {A B : Set}
-  → (eqv @ (f , f-eqv) : A ≃ B)
-  → (a a' : A)
-  → (a ≡ a') ≃ (f a ≡ f a')
-theorem2∙11∙1 (f , f-eqv) a a' =
-  let
-    open ≡-Reasoning
-    mkQinv g α β = isequiv-to-qinv f-eqv
-    inv : (f a ≡ f a') → a ≡ a'
-    inv p = (sym (β a)) ∙ (ap g p) ∙ (β a')
-    backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
-    backward q = begin
-      ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a')  ⟩
-      ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
-      ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
-      id q ∎
-    forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
-    forward p = begin
-      (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩
-      (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {!   !} ⟩
-      -- (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {!   !} ⟩
-      id p ∎
-    eqv = mkQinv inv backward forward
-  in
-  ap f , qinv-to-isequiv eqv
+-- theorem2∙11∙1 : {A B : Set}
+--   → (eqv @ (f , f-eqv) : A ≃ B)
+--   → (a a' : A)
+--   → (a ≡ a') ≃ (f a ≡ f a')
+-- theorem2∙11∙1 (f , f-eqv) a a' =
+--   let
+--     open ≡-Reasoning
+--     mkQinv g α β = isequiv-to-qinv f-eqv
+--     inv : (f a ≡ f a') → a ≡ a'
+--     inv p = (sym (β a)) ∙ (ap g p) ∙ (β a')
+--     backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
+--     backward q = begin
+--       ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a')  ⟩
+--       ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
+--       ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
+--       id q ∎
+--     forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
+--     forward p = begin
+--       (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩
+--       (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {!   !} ⟩
+--       -- (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {!   !} ⟩
+--       id p ∎
+--     eqv = mkQinv inv backward forward
+--   in
+--   ap f , qinv-to-isequiv eqv
 ```
 
 ### Theorem 2.11.2
 
 ```
--- module theorem2∙11∙2 where
---   i : {A : Set} {a x1 x2 : A}
---     → (p : x1 ≡ x2)
---     → (q : a ≡ x1)
---     → transport (λ y → a ≡ y) p q ≡ q ∙ p
---   i {A} {a} {x1} {x2} p q =
---     J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1)
---       (λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → {!  refl !}) a x3 q1)
---       x1 x2 p q
+module theorem2∙11∙2 where
+  open ≡-Reasoning
+
+  i : {A : Set} {a x1 x2 : A}
+    → (p : x1 ≡ x2)
+    → (q : a ≡ x1)
+    → transport (λ y → a ≡ y) p q ≡ q ∙ p
+  i {A} {a} {x1} {x2} p q =
+    J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1)
+      (λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → lemma2∙1∙4.i1 q1) a x3 q1)
+      x1 x2 p q
+
+  ii : {A : Set} {a x1 x2 : A}
+    → (p : x1 ≡ x2)
+    → (q : x1 ≡ a)
+    → transport (λ y → y ≡ a) p q ≡ sym p ∙ q
+  ii {A} {a} {x1} {x2} p q = 
+    J (λ x y p → (q1 : x ≡ a) → transport (λ y → y ≡ a) p q1 ≡ sym p ∙ q1)
+      (λ x q1 → J (λ x y p → transport (λ y → y ≡ a) refl q1 ≡ sym refl ∙ q1) (λ x → lemma2∙1∙4.i2 q1) x a q1)
+      x1 x2 p q
+
+  iii : {A : Set} {a x1 x2 : A}
+    → (p : x1 ≡ x2)
+    → (q : x1 ≡ x1)
+    → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
+  iii {A} {a} {x1} {x2} p q =
+    J (λ x y p → (q1 : x ≡ x) → transport (λ y → y ≡ y) p q1 ≡ sym p ∙ q1 ∙ p)
+      (λ x q1 → J (λ x y p → transport (λ y → y ≡ y) refl q1 ≡ sym refl ∙ q1 ∙ refl)
+        (λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper)
+        x x q1)
+      x1 x2 p q
 ```
 
 ### Theorem 2.11.3
@@ -786,7 +808,41 @@ theorem2∙11∙3 : {A B : Set} → {f g : A → B} → {a a' : A}
   → (p : a ≡ a')
   → (q : f a ≡ g a)
   → transport (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ (ap g p)
-theorem2∙11∙3 p q = {!   !}
+theorem2∙11∙3 {A} {B} {f} {g} {a} {a'} p q =
+  J (λ x y p → (q1 : f x ≡ g x) → transport (λ x → f x ≡ g x) p q1 ≡ sym (ap f p) ∙ q1 ∙ (ap g p))
+    (λ x q1 →
+      J (λ x y p → transport (λ z → f z ≡ g z) refl q1 ≡ sym (ap f refl) ∙ q1 ∙ ap g refl)
+        (λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper)
+        (f a) (g a) q)
+    a a' p q
+```
+
+### Theorem 2.11.4
+
+```
+theorem2∙11∙4 : {A : Set} {B : A → Set} {f g : (x : A) → B x} {a a' : A}
+  → (p : a ≡ a')
+  → (q : f a ≡ g a)
+  → transport (λ x → f x ≡ g x) p q ≡ sym (apd f p) ∙ ap (transport B p) q ∙ apd g p
+theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} p q =
+  let open ≡-Reasoning in
+  J (λ x y p → (q1 : f x ≡ g x) → transport (λ x → f x ≡ g x) p q1 ≡ sym (apd f p) ∙ ap (transport B p) q1 ∙ apd g p)
+    (λ x q1 →
+      J (λ x y p → transport (λ z → f z ≡ g z) refl q1 ≡ sym (apd f refl) ∙ ap (transport B refl) q1 ∙ apd g refl)
+        (λ y → 
+          let
+            q2 = ap id q1
+            q1≡q2 : q1 ≡ q2
+            q1≡q2 = J (λ a b p → p ≡ ap id p) (λ x → refl) (f x) (g x) q1
+          in
+          begin
+            transport (λ z → f z ≡ g z) refl q1 ≡⟨⟩
+            q1 ≡⟨ q1≡q2 ⟩
+            q2 ≡⟨ (let helper = ap (λ p → refl ∙ p) (lemma2∙1∙4.i1 q2) in lemma2∙1∙4.i2 q2 ∙ helper) ⟩
+            refl ∙ ap (transport B refl) q1 ∙ refl ∎
+        )
+        (f a) (g a) q)
+    a a' p q
 ```
 
 ## 2.12 Coproducts
diff --git a/src/HottBook/Chapter2.pdf b/src/HottBook/Chapter2.pdf
new file mode 100644
index 0000000..e1a1a37
Binary files /dev/null and b/src/HottBook/Chapter2.pdf differ
diff --git a/src/HottBook/Chapter2.typ b/src/HottBook/Chapter2.typ
new file mode 100644
index 0000000..cf92f13
--- /dev/null
+++ b/src/HottBook/Chapter2.typ
@@ -0,0 +1,59 @@
+#import "@preview/cetz:0.2.2"
+#set page(width: auto, height: auto, margin: .5cm)
+
+#let data = (
+  ([Belgium],     24),
+  ([Germany],     31),
+  ([Greece],      18),
+  ([Spain],       21),
+  ([France],      23),
+  ([Hungary],     18),
+  ([Netherlands], 27),
+  ([Romania],     17),
+  ([Finland],     26),
+  ([Turkey],      13),
+)
+
+#cetz.canvas({
+  import cetz.chart
+  import cetz.draw: *
+
+  // let colors = gradient.linear(red, blue, green, yellow)
+
+  // chart.piechart(
+  //   data,
+  //   value-key: 1,
+  //   label-key: 0,
+  //   radius: 4,
+  //   slice-style: colors,
+  //   inner-radius: 1,
+  //   outset: 3,
+  //   inner-label: (content: (value, label) => [#text(white, str(value))], radius: 110%),
+  //   outer-label: (content: "%", radius: 110%))
+
+  let point(p, name) = {
+    content((p.at(0)-0.1, p.at(1)+0.1), name)
+    circle(p, radius: 0.05, fill: black)
+  }
+
+  circle((2, 1), radius: (1, 1), fill: gray, stroke: none)
+  circle((2, 3), radius: (1, 0.75), fill: gray, stroke: none)
+
+  let a = (1.6, 3)
+  let b = (2.4, 3)
+
+  let fa = (1.6, 1.5)
+  let fb = (2.4, 1.5)
+  let ga = (1.3, 0.5)
+  let gb = (2.7, 0.5)
+
+  point(a, "a")
+  point(b, "b")
+  point(fa, "f(a)")
+  point(fb, "f(b)")
+  point(ga, "g(a)")
+  point(gb, "g(b)")
+
+  line(a, fa)
+  
+})
\ No newline at end of file
diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 341d88e..9b31abe 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -4,7 +4,6 @@ module HottBook.Chapter2Exercises where
 open import Agda.Primitive
 open import HottBook.Chapter1
 open import HottBook.Chapter2
-open import HottBook.Chapter2Lemma221
 open import HottBook.Util
 ```
 
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 7292f4b..88deb69 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -5,7 +5,6 @@ open import Agda.Primitive
 open import HottBook.Chapter1
 open import HottBook.Chapter1Util
 open import HottBook.Chapter2
-open import HottBook.Chapter2Lemma221
 open import HottBook.Chapter3Definition331
 open import HottBook.Chapter3Lemma333
 open import HottBook.Util
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index 280eb94..06a3e7d 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -3,7 +3,6 @@ module HottBook.Chapter6 where
 
 open import HottBook.Chapter1
 open import HottBook.Chapter2
-open import HottBook.Chapter2Lemma221
 ```
 
 # 6 Higher inductive types
diff --git a/src/MayConcise/Chapter1.lagda.md b/src/MayConcise/Chapter1.lagda.md
index 085e298..a4661fd 100644
--- a/src/MayConcise/Chapter1.lagda.md
+++ b/src/MayConcise/Chapter1.lagda.md
@@ -29,5 +29,4 @@ https://en.wikipedia.org/wiki/Homomorphism
 ## 4 Homotopy invariance
 
 ```
-_⋆ 
 ```
\ No newline at end of file