diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 52c6a2f..6c79ab6 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -149,11 +149,13 @@ lemma2∙3∙8 {l} {A} {B} f {x} {y} p =
 ### Lemma 2.3.11
 
 ```
--- lemma2311 : {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)
--- lemma2311 {A} {P} {Q} f {x} {y} p u =
---   J (λ the what → transport Q what (f x u) ≡ f the (transport P what u)) p refl
+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 (λ a b p → transport Q p (f a {!   !}) ≡ f b (transport P p {!   !})) (λ a → {!   !}) x y p
+  -- J (λ the what → transport Q what (f x u) ≡ f the (transport P what u)) p refl
 ```
 
 ## 2.4 Homotopies and equivalences