From 628e0d9e9fc651f21f89da9b02f1bcf1b9f40ab2 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 30 May 2024 15:48:39 -0500 Subject: [PATCH] theorem 2.13.1 --- src/HottBook/Chapter2.lagda.md | 95 +++++++++++++--------------------- 1 file changed, 35 insertions(+), 60 deletions(-) diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 6248f85..59017b3 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -904,79 +904,54 @@ remark2∙12∙6 p = genBot tt ## 2.13 Natural numbers ``` -private - code : ℕ → ℕ → Set - code zero zero = 𝟙 - code zero (suc y) = ⊥ - code (suc x) zero = ⊥ - code (suc x) (suc y) = code x y ``` ### Theorem 2.13.1 _For all $m, n : N$ we have $(m = n) \simeq \texttt{code}(m, n)$._ -```text -theorem2∙13∙1 : (m n : ℕ) → (m ≡ n) ≃ code m n -theorem2∙13∙1 m n = encode m n , equiv - where - r : (n : ℕ) → code n n - r zero = tt - r (suc n) = r n +``` +module 2∙13∙1 where + open ≡-Reasoning - encode : (m n : ℕ) → m ≡ n → code m n - encode m n p = transport (λ n → code m n) p (r m) + code : ℕ → ℕ → Set + code zero zero = 𝟙 + code zero (suc y) = ⊥ + code (suc x) zero = ⊥ + code (suc x) (suc y) = code x y - decode : (m n : ℕ) → code m n → m ≡ n - decode zero zero c = refl - decode (suc m) (suc n) c = ap suc (decode m n c) + r : (n : ℕ) → code n n + r zero = tt + r (suc n) = r n - forward : (m n : ℕ) → (p : m ≡ n) → (encode m n ∘ decode m n) p ≡ id p - forward m n p = J C c m n p - where - C : (x y : ℕ) → (p : x ≡ y) → Set - C x y p = (encode x y ∘ decode x y) p ≡ id p + encode : (m n : ℕ) → m ≡ n → code m n + encode m n p = transport (code m) p (r m) - c : (x : ℕ) → decode x x (r x) ≡ refl - c zero = refl - c (suc x) = ap (λ p → ap suc p) (c x) + decode : (m n : ℕ) → code m n → m ≡ n + decode zero zero tt = refl + decode (suc m) (suc n) c = ap suc (decode m n c) - backward : (m n : ℕ) → (c : code m n) → (decode m n ∘ encode m n) c ≡ id c - backward zero zero c = - let - what = encode zero zero refl - what2 = decode zero zero c - what3 = theorem2∙8∙1 what c - what4 = isequiv.g (Σ.snd what3) - what5 = what4 tt - in what5 - backward (suc m) (suc n) c = - let - IH = backward m n c + backward : (m n : ℕ) → (c : code m n) → encode m n (decode m n c) ≡ c + backward zero zero tt = refl + backward (suc m) (suc n) c = + begin + encode (suc m) (suc n) (decode (suc m) (suc n) c) ≡⟨⟩ + encode (suc m) (suc n) (ap suc (decode m n c)) ≡⟨⟩ + transport (code (suc m)) (ap suc (decode m n c)) (r (suc m)) ≡⟨ sym (lemma2∙3∙10 suc (code (suc m)) (decode m n c) (r (suc m))) ⟩ + transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m)) ≡⟨⟩ + transport (code m) (decode m n c) (r m) ≡⟨⟩ + encode m n (decode m n c) ≡⟨ backward m n c ⟩ + c ∎ - -- what : code m n - -- what = encode (suc m) (suc n) (ap suc (decode m n c)) - -- what = transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m)) - -- what = transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m)) - -- what = transport (λ n → code m n) (decode m n c) (r m) - -- what = transport (λ n → code m n) (decode m n c) (r m) - -- what = transport (λ n → code m n) (decode m n c) (r m) + 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 + where + f : (x : ℕ) → decode x x (r x) ≡ refl + f zero = refl + f (suc x) = ap (ap suc) (f x) - res2 : transport (λ x → code (suc m) (suc x)) (decode m n c) (r (suc m)) ≡ c - res2 = IH - - -- res : encode (suc m) (suc n) (ap suc (decode m n c)) ≡ c - res : transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m)) ≡ c - res = - - in res - - equiv = record - { g = decode m n - ; g-id = forward m n - ; h = decode m n - ; h-id = backward m n - } + theorem2∙13∙1 : (m n : ℕ) → (m ≡ n) ≃ code m n + theorem2∙13∙1 m n = encode m n , qinv-to-isequiv (mkQinv (decode m n) (backward m n) (forward m n)) ``` ## 2.15 Universal properties