From 18e037341af79e49da6529ee013fc4979e42dc14 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 31 May 2024 20:17:22 -0500 Subject: [PATCH] rewrite verbose J --- src/HottBook/Chapter2.lagda.md | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index cd8c014..a02609b 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -841,30 +841,19 @@ module lemma2∙11∙2 where → (p : x1 ≡ x2) → (q : a ≡ x1) → transport (λ y → a ≡ y) p q ≡ q ∙ p - i {l} {A} {a} {x1} {x2} p q = - J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1) - (λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → lemma2∙1∙4.i1 q1) a x3 q1) - x1 x2 p q + i {l} {A} {a} {x1} {x2} refl refl = refl ii : {l : Level} {A : Set l} {a x1 x2 : A} → (p : x1 ≡ x2) → (q : x1 ≡ a) → transport (λ y → y ≡ a) p q ≡ sym p ∙ q - ii {l} {A} {a} {x1} {x2} p q = - J (λ x y p → (q1 : x ≡ a) → transport (λ y → y ≡ a) p q1 ≡ sym p ∙ q1) - (λ x q1 → J (λ x y p → transport (λ y → y ≡ a) refl q1 ≡ sym refl ∙ q1) (λ x → lemma2∙1∙4.i2 q1) x a q1) - x1 x2 p q + ii {l} {A} {a} {x1} {x2} refl refl = refl iii : {l : Level} {A : Set l} {a x1 x2 : A} → (p : x1 ≡ x2) → (q : x1 ≡ x1) → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p - iii {l} {A} {a} {x1} {x2} p q = - J (λ x y p → (q1 : x ≡ x) → transport (λ y → y ≡ y) p q1 ≡ sym p ∙ q1 ∙ p) - (λ x q1 → J (λ x y p → transport (λ y → y ≡ y) refl q1 ≡ sym refl ∙ q1 ∙ refl) - (λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper) - x x q1) - x1 x2 p q + iii {l} {A} {a} {x1} {x2} refl refl = refl ``` ### Theorem 2.11.3 @@ -1010,7 +999,7 @@ module theorem2∙13∙1 where c ∎ forward : (m n : ℕ) → (p : m ≡ n) → decode m n (encode m n p) ≡ p - forward m n p = J (λ x y p → decode x y (encode x y p) ≡ p) f m n p + forward m n refl = f m where f : (x : ℕ) → decode x x (r x) ≡ refl f zero = refl