diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index a02609b..9a24e62 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -19,23 +19,15 @@ open import HottBook.Util
 ### Lemma 2.1.1
 
 ```
-sym : {l : Level} {A : Set l} {x y : A}
-  → (x ≡ y) → y ≡ x
-sym {l} {A} {x} {y} p = J (λ x y p → y ≡ x) (λ x → refl) x y p
+sym : {l : Level} {A : Set l} {x y : A} → (x ≡ y) → y ≡ x
+sym {l} {A} {x} {y} refl = refl
 ```
 
 ### Lemma 2.1.2
 
 ```
-trans : {l : Level} {A : Set l} {x y z : A}
-  → (x ≡ y)
-  → (y ≡ z)
-  → (x ≡ z)
-trans {l} {A} {x} {y} {z} p q =
-  let
-    func1 x y p = J (λ a b p → a ≡ b) (λ x → refl) x y p
-    func2 = J (λ a b p → (z : A) → (q : b ≡ z) → a ≡ z) func1 x y p
-  in func2 z q
+trans : {l : Level} {A : Set l} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
+trans {l} {A} {x} {y} {z} refl refl = refl
 
 infixr 30 _∙_
 _∙_ = trans
@@ -67,33 +59,22 @@ module ≡-Reasoning where
 ```
 module lemma2∙1∙4 {l : Level} {A : Set l} where
   i1 : {x y : A} (p : x ≡ y) → p ≡ p ∙ refl
-  i1 {x} {y} p = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p
+  i1 {x} {y} refl = refl
 
   i2 : {x y : A} (p : x ≡ y) → p ≡ refl ∙ p
-  i2 {x} {y} p = J (λ x y p → p ≡ refl ∙ p) (λ _ → refl) x y p
+  i2 {x} {y} refl = refl
 
   ii1 : {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
-  ii1 {x} {y} p = J (λ x y p → (sym p) ∙ p ≡ refl) (λ _ → refl) x y p
+  ii1 {x} {y} refl = refl
 
   ii2 : {x y : A} (p : x ≡ y) → p ∙ (sym p) ≡ refl
-  ii2 {x} {y} p = J (λ x y p → p ∙ (sym p) ≡ refl) (λ _ → refl) x y p
+  ii2 {x} {y} refl = refl
 
   iii : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
-  iii {x} {y} p = J (λ x y p → sym (sym p) ≡ p) (λ _ → refl) x y p
+  iii {x} {y} refl = refl
 
   iv : {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
-  iv {x} {y} {z} {w} p q r = let
-      open ≡-Reasoning
-
-      C : (x y : A) → (p : x ≡ y) → Set l
-      C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
-
-      c : (x : A) → C x x refl
-      c x q1 = begin
-        refl ∙ (q1 ∙ r) ≡⟨ sym (i2 (q1 ∙ r)) ⟩
-        (q1 ∙ r) ≡⟨ ap (λ p → p ∙ r) (i2 q1) ⟩
-        (refl ∙ q1) ∙ r ∎
-    in J C c x y p q
+  iv {x} {y} {z} {w} refl refl refl = refl
 ```
 
 ### Definition 2.1.7 (pointed type)
@@ -144,21 +125,16 @@ module lemma2∙2∙2 {A B C : Set} where
   open ≡-Reasoning
 
   i : {f : A → B} {x y z : A} (p : x ≡ y) (q : y ≡ z) → ap f (p ∙ q) ≡ ap f p ∙ ap f q
-  i {f} {x} {y} {z} p q = J
-    ((λ x1 y1 p1 → (q1 : y1 ≡ z) → ap f (p1 ∙ q1) ≡ ap f p1 ∙ ap f q1))
-    (λ x1 q1 → J
-      (λ x2 y2 p2 → ap f (refl ∙ p2) ≡ ap f refl ∙ ap f p2)
-      (λ x2 → refl) x1 z q1
-    ) x y p q
+  i {f} {x} {y} {z} refl refl = refl
 
   ii : {f : A → B} {x y : A} (p : x ≡ y) → ap f (sym p) ≡ sym (ap f p)
-  ii {f} {x} {y} p = J (λ x1 y1 p1 → ap f (sym p1) ≡ sym (ap f p1)) (λ x1 → refl) x y p
+  ii {f} {x} {y} refl = refl
 
   iii : (f : A → B) (g : B → C) {x y : A} (p : x ≡ y) → ap g (ap f p) ≡ ap (g ∘ f) p
-  iii f g {x} {y} p = J (λ x1 y1 p1 → ap g (ap f p1) ≡  ap (g ∘ f) p1) (λ x1 → refl) x y p
+  iii f g {x} {y} refl = refl
 
   iv : {x y : A} (p : x ≡ y) → ap id p ≡ p
-  iv {x} {y} p = J (λ x1 y1 p1 → ap id p1 ≡ p1) (λ x1 → refl) x y p
+  iv {x} {y} refl = refl
 ```
 
 ## 2.3 Type families are fibrations
@@ -170,24 +146,19 @@ transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
   → (P : A → Set l₂)
   → (p : x ≡ y)
   → P x → P y
-transport {l₁} {l₂} {A} {x} {y} P p = J (λ x y p → P x → P y) (λ x → id) x y p
+transport {l₁} {l₂} {A} {x} {y} P refl = id
 ```
 
 ### Lemma 2.3.2 (Path lifting property)
 
-```
-lift : {A : Set} {P : A → Set} {x y : A}
-  → (u : P x)
-  → (p : x ≡ y)
-  → (x , u) ≡ (y , transport P p u)
-lift {A} {P} {x} {y} u p =
-  J (λ x1 y1 p1 → (u1 : P x1) → (x1 , u1) ≡ (y1 , transport P p1 u1)) (λ x1 u1 → refl) x y p u
-```
-
-Verifying its property:
-
 ```
 module lemma2∙3∙2 where
+  lift : {A : Set} {P : A → Set} {x y : A}
+    → (u : P x)
+    → (p : x ≡ y)
+    → (x , u) ≡ (y , transport P p u)
+  lift {A} {P} {x} {y} u refl = refl
+
   pr₁ : {A : Set} {P : A → Set}
     {x y : A}
     {u : P x} {v : P y}
@@ -199,8 +170,7 @@ module lemma2∙3∙2 where
 
   lift-prop : {A : Set} {P : A → Set} {x y : A} (u : P x) → (p : x ≡ y)
     → pr₁ (lift {A} {P} u p) ≡ p
-  lift-prop {A} {P} {x} {y} u p =
-    J (λ x1 y1 p1 → (u1 : P x1) → pr₁ (lift {A} {P} u1 p1) ≡ p1) (λ x1 u1 → refl) x y p u
+  lift-prop {A} {P} {x} {y} u refl = refl
 ```
 
 ### Lemma 2.3.4 (Dependent map)
@@ -210,8 +180,7 @@ apd : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂} {x y : A}
   → (f : (x : A) → P x)
   → (p : x ≡ y)
   → transport P p (f x) ≡ f y
-apd {l₁} {l₂} {A} {P} {x} {y} f p =
-  J (λ x y p → transport P p (f x) ≡ f y) (λ x → refl) x y p
+apd {l₁} {l₂} {A} {P} {x} {y} f refl = refl
 ```
 
 ### Lemma 2.3.5
@@ -222,8 +191,7 @@ transportconst : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
   → (p : x ≡ y)
   → (b : B)
   → transport (λ _ → B) p b ≡ b
-transportconst {l₁} {l₂} {A} {x} {y} B p b =
-  J (λ x y p → transport (λ _ → B) p b ≡ b) (λ x → refl) x y p
+transportconst {l₁} {l₂} {A} {x} {y} B refl b = refl
 ```
 
 ### Equation 2.3.6
@@ -252,8 +220,7 @@ lemma2∙3∙8 : {l : Level} {A B : Set l}
   → {x y : A} 
   → (p : x ≡ y)
   → apd f p ≡ transportconst B p (f x) ∙ ap f p
-lemma2∙3∙8 {l} {A} {B} f {x} {y} p =
-  J (λ x y p → apd f p ≡ transportconst B p (f x) ∙ ap f p) (λ x → refl) x y p
+lemma2∙3∙8 {l} {A} {B} f {x} {y} refl = refl
 ```
 
 ### Lemma 2.3.9
@@ -264,13 +231,7 @@ lemma2∙3∙9 : {A : Set}
   → (P : A → Set)
   → (p : x ≡ y) → (q : y ≡ z) → (u : P x)
   → transport P q (transport P p u) ≡ transport P (p ∙ q) u
-lemma2∙3∙9 {A} {x} {y} {z} P p q u = 
-  let 
-    f2 : (x1 : A) → (q1 : x1 ≡ z) (u1 : P x1) → transport P q1 u1 ≡ transport P (refl ∙ q1) u1
-    f2 x1 q1 u1 =
-      ap (λ x → transport P x u1) (lemma2∙1∙4.i2 q1)
-    f1 = J (λ x1 y1 p1 → (q1 : y1 ≡ z) → (u1 : P x1) → transport P q1 (transport P p1 u1) ≡ transport P (p1 ∙ q1) u1) f2 x y p
-  in f1 q u
+lemma2∙3∙9 {A} {x} {y} {z} P refl refl u = refl
 ```
 
 ### Lemma 2.3.10
@@ -283,9 +244,7 @@ lemma2∙3∙10 : {l1 l2 : Level} {A B : Set l1}
   → (p : x ≡ y)
   → (u : P (f x))
   → transport (P ∘ f) p u ≡ transport P (ap f p) u
-lemma2∙3∙10 {l} {A} {B} f P {x} {y} p u =
-  J (λ x1 y1 p1 → (u1 : P (f x1)) → transport (P ∘ f) p1 u1 ≡ transport P (ap f p1) u1)
-    (λ x1 u1 → refl) x y p u
+lemma2∙3∙10 {l} {A} {B} f P {x} {y} refl u = refl
 ```
 
 ### Lemma 2.3.11
@@ -295,9 +254,7 @@ lemma2∙3∙11 : {A : Set} {P Q : A → Set}
   → (f : (x : A) → P x → Q x)
   → {x y : A} (p : x ≡ y) → (u : P x)
   → transport Q p (f x u) ≡ f y (transport P p u)
-lemma2∙3∙11 {A} {P} {Q} f {x} {y} p u =
-  J (λ x1 y1 p1 → (u1 : P x1) → transport Q p1 (f x1 u1) ≡ f y1 (transport P p1 u1))
-    (λ x1 u1 → refl) x y p u
+lemma2∙3∙11 {A} {P} {Q} f {x} {y} refl u = refl
 ```
 
 ## 2.4 Homotopies and equivalences
@@ -340,16 +297,14 @@ Homotopy forms an equivalence relation:
 ```
 lemma2∙4∙3 : {A B : Set} {f g : A → B} (H : f ∼ g) {x y : A} (p : x ≡ y)
   → H x ∙ ap g p ≡ ap f p ∙ H y
-lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} p = let
-    open ≡-Reasoning
-  in
-  J (λ x1 y1 p1 → (H x1 ∙ ap g p1 ≡ ap f p1 ∙ H y1)) (λ x1 → begin
-    H x1 ∙ ap g refl ≡⟨⟩
-    H x1 ∙ refl ≡⟨ sym (lemma2∙1∙4.i1 (H x1)) ⟩
-    H x1 ≡⟨ lemma2∙1∙4.i2 (H x1) ⟩
-    refl ∙ H x1 ≡⟨⟩
-    ap f refl ∙ H x1 ∎
-  ) x y p
+lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} refl =
+  let open ≡-Reasoning in
+  begin
+    H x ∙ ap g refl ≡⟨⟩
+    H x ∙ refl ≡⟨ sym (lemma2∙1∙4.i1 (H x)) ⟩
+    H x ≡⟨ lemma2∙1∙4.i2 (H x) ⟩
+    refl ∙ H x ≡⟨⟩
+    ap f refl ∙ H x ∎
 ```
 
 ### Corollary 2.4.4
@@ -704,9 +659,7 @@ equation2∙9∙4 : {l1 l2 : Level} {X : Set l1} {x1 x2 : X}
   → (f : A x1 → B x1)
   → (p : x1 ≡ x2)
   → transport (λ x → A x → B x) p f ≡ λ x → transport B p (f (transport A (sym p) x))
-equation2∙9∙4 {l1} {l2} {X} {x1} {x2} {A} {B} f p =
-  J (λ x3 y3 p1 → (f1 : A x3 → B x3) → (transport (λ x → A x → B x) p1 f1 ≡ λ x → transport B p1 (f1 (transport A (sym p1) x))))
-  (λ x3 f1 → refl) x1 x2 p f
+equation2∙9∙4 {l1} {l2} {X} {x1} {x2} {A} {B} f refl = refl
 ```
 
 ### Equation 2.9.5
@@ -730,9 +683,7 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where
     → (p : x1 ≡ x2)
     → (a : A x2)
     → 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-≡-d (sym p') refl)) (f' (transport A (sym p') a')))
-      (λ x' f' a' → refl) x1 x2 p f a
+  equation2∙9∙5 A B f refl a = refl
 ```
 
 ### Lemma 2.9.6
@@ -761,13 +712,6 @@ idtoeqv : {l : Level} {A B : Set l}
   → (A ≡ B)
   → (A ≃ B)
 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
 ```
 
 ### Axiom 2.10.3 (Univalence)
@@ -863,13 +807,9 @@ 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 {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
+theorem2∙11∙3 {A} {B} {f} {g} {a} {a'} refl q =
+  let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q) in
+  lemma2∙1∙4.i2 q ∙ helper
 ```
 
 ### Theorem 2.11.4
@@ -879,25 +819,18 @@ 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
+theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} refl q = 
+  let
+    open ≡-Reasoning
+    q2 = ap id q
+    q≡q2 : q ≡ q2
+    q≡q2 = J (λ a b p → p ≡ ap id p) (λ x → refl) (f a) (g a) q
+  in
+  begin
+    transport (λ z → f z ≡ g z) refl q ≡⟨⟩
+    q ≡⟨ q≡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) q ∙ refl ∎
 ```
 
 ### Theorem 2.11.5