diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 312df30..52c6a2f 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -56,12 +56,12 @@ transport {l₁} {l₂} {A} {x} {y} P p = J (λ x y p → P x → P y) (λ x →
 TODO
 
 ```
-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 (λ a b p → (a , {!  !}) ≡ (b , {!   !})) (λ x → {!   !}) x y p
+-- 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 (λ a b p → (x , {!  !}) ≡ (y , {!   !})) (λ x → {!   !}) x y p
 ```
 
 Verifying its property: