update

src/HottBook/Chapter2.lagda.md

@@ -136,9 +136,25 @@ TODO
 Ap rules
 
 ```
--- module lemma2∙2∙2 {A B : Set} {f : A → B} {x y z : A} {p : x ≡ y} {q : y ≡ z} where
---   i : ap f (p ∙ q) ≡ ap f p ∙ ap f q
---   i = J ((λ x1 y1 p1 → (q1 : y1 ≡ z) → ap f (p1 ∙ q1) ≡ ap f p1 ∙ ap f q1)) (λ x1 q1 → {!   !}) x y p q
+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
+
+  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
+
+  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
+
+  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
 ```
 
 ## 2.3 Type families are fibrations
@@ -155,24 +171,32 @@ transport {l₁} {l₂} {A} {x} {y} P p = J (λ x y p → P x → P y) (λ x →
 
 ### Lemma 2.3.2 (Path lifting property)
 
-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 → (x , {!  !}) ≡ (y , {!   !})) (λ 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 (λ x1 y1 p1 → (u1 : P x1) → (x1 , u1) ≡ (y1 , transport P p1 u1)) (λ x1 u1 → refl) x y p u
 ```
 
 Verifying its property:
 
 ```
--- lift-prop : {A : Set} (P : A → Set) {x y : A} (u : P x) → (p : x ≡ y)
---   → Σ.fst (Σ-≡,≡←≡ (lift P u p)) ≡ p
--- lift-prop P u p =
---   J (λ the what → proj₁ (Σ-≡,≡←≡ (lift P u what)) ≡ what) p refl
+module lemma2∙3∙2 where
+  pr₁ : {A : Set} {P : A → Set}
+    {x y : A}
+    {u : P x} {v : P y}
+    (p : (x , u) ≡ (y , v))
+    → x ≡ y
+  pr₁ p = ap (λ (x , y) → x) p
+
+  open ≡-Reasoning
+
+  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
 ```
 
 ### Lemma 2.3.4 (Dependent map)
@@ -188,8 +212,6 @@ apd {l₁} {l₂} {A} {P} {x} {y} f p =
 
 ### Lemma 2.3.5
 
-TODO
-
 ```
 transportconst : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
   → (B : Set l₂)
@@ -562,15 +584,21 @@ postulate
 -- theorem2∙11∙1 (f , f-eqv) a a' =
 --   let
 --     open ≡-Reasoning
---     mkQinv f⁻¹ α β = isequiv-to-qinv f-eqv
+--     mkQinv g α β = isequiv-to-qinv f-eqv
 --     inv : (f a ≡ f a') → a ≡ a'
---     inv p = (sym (β a)) ∙ (ap f⁻¹ p) ∙ (β a')
+--     inv p = (sym (β a)) ∙ (ap g p) ∙ (β a')
 --     backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
 --     backward q = begin
---       ap f ((sym (β a)) ∙ (ap f⁻¹ q) ∙ (β a')) ≡⟨ {!   !} ⟩
+--       ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a')  ⟩
+--       ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
+--       ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
 --       id q ∎
 --     forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
---     forward p = {!   !}
+--     forward p = begin
+--       (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩
+--       (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {!   !} ⟩
+--       (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {!   !} ⟩
+--       id p ∎
 --     eqv = mkQinv inv backward forward
 --   in
 --   ap f , qinv-to-isequiv eqv