diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 73fe35a..8d3e521 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -589,14 +589,17 @@ corollary2∙7∙3 z = refl
 ### Theorem 2.7.4
 
 ```
--- theorem2∙7∙4 : {A : Set} {P : A → Set}
---   → (Q : Σ A (λ x → P x) → Set)
---   → {x y : A}
---   → (p : x ≡ y)
---   → (u z : Σ (P x) (λ u → Q (x , u)))
---   → transport (λ x → Σ (Σ (P x) λ u → Q (x , u)) λ _ → Σ (P x) λ u → Q (x , u)) p (u , z)
---     ≡ ( transport (λ x → Σ (P x) λ u → Q (x , u)) p u
---       , transport (λ (m , n) → {! Σ (P y) ? !}) (Σ-≡ (p , refl)) z)
+-- module theorem2∙7∙4 where
+--   private
+--     TF = λ P Q x → Σ (P x) (λ u → Q (x , u))
+
+--   theorem2∙7∙4 : {A : Set} {P : A → Set}
+--     → (Q : Σ A P → Set)
+--     → {x y : A}
+--     → (p : x ≡ y)
+--     → (u z : Σ (P x) (λ u → Q (x , u)))
+--     → transport (λ r → Σ {!    !} {!   !}) p (u , z) ≡ (transport {!   !} p u , transport {! TF P Q  !} (pair-≡ (p , refl)) z)
+--   theorem2∙7∙4 Q refl u z = refl
 ```
 
 ## 2.8 The unit type