exercise 2.18

src/HottBook/Chapter2.lagda.md

@@ -120,8 +120,10 @@ module theorem2∙1∙6 where
 Ap rules
 
 ```
-module lemma2∙2∙2 {A B C : Set} where
-  open ≡-Reasoning
+module lemma2∙2∙2 where
+  private
+    variable
+      A B C : Set
 
   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} refl refl = refl

src/HottBook/Chapter2Exercises.lagda.md

@@ -13,6 +13,8 @@ Show that the three obvious proofs of Lemma 2.1.2 are pair- wise equal.
 
 ```
 module exercise2∙1 {l : Level} {A : Set l} where
+  open axiom2∙9∙3
+
   prf1 : {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
   prf1 refl q = q
 
@@ -143,6 +145,8 @@ exercise2∙9 : {A B X : Set} → (A + B → X) ≃ ((A → X) × (B → X))
 exercise2∙9 {A} {B} {X} =
   f , qinv-to-isequiv (mkQinv g f∘g∼id g∘f∼id)
   where
+    open axiom2∙9∙3
+
     f : (A + B → X) → (A → X) × (B → X) 
     f func = (λ a → func (inl a)) , (λ b → func (inr b))
 
@@ -208,6 +212,7 @@ main proof:
 exercise2∙13 : (𝟚 ≃ 𝟚) ≃ 𝟚
 exercise2∙13 = f , equiv
   where
+    open axiom2∙9∙3
     open WithAbstractionUtil
 
     f : 𝟚 ≃ 𝟚 → 𝟚
@@ -325,3 +330,23 @@ module exercise2∙17 where
       combined-id = pair-≡ A-id B-id
    in idtoeqv combined-id
 ``` 
+
+## Exercise 2.18
+
+```
+exercise2∙18 : {A : Set} {B : A → Set} {f g : (x : A) → B x} (H : f ∼ g) {x y : A} (p : x ≡ y)
+  → ap (transport B p) (H x) ∙ apd g p ≡ apd f p ∙ (H y)
+exercise2∙18 {A = A} {B = B} {f = f} {g = g} H {x = x} {y = y} refl =
+  let 
+    open ≡-Reasoning
+    open axiom2∙9∙3
+  in
+  begin
+    ap (transport B refl) (H x) ∙ apd g refl ≡⟨⟩
+    ap id (H x) ∙ apd g refl ≡⟨⟩
+    ap id (H x) ∙ refl ≡⟨ sym (lemma2∙1∙4.i1 (ap id (H x))) ⟩
+    ap id (H x) ≡⟨ lemma2∙2∙2.iv (H x) ⟩
+    H x ≡⟨ lemma2∙1∙4.i2 (H x) ⟩
+    refl ∙ H x ≡⟨⟩
+    apd f refl ∙ H x ∎
+```