theorem 2.13.1

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