# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686190880 -32400
# Node ID 81f66cec617ea2f492dd83f35fd0e17b9c985223
# Parent  f832e986427dbebb4b5951c408e38a1d325933f9
...

diff -r f832e986427d -r 81f66cec617e src/bijection.agda
--- a/src/bijection.agda	Wed Jun 07 11:26:03 2023 +0900
+++ b/src/bijection.agda	Thu Jun 08 11:21:20 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
+{-# OPTIONS --allow-unsolved-metas #-}
 
 module bijection where
 
@@ -22,13 +22,13 @@
 --    field
 --        fun←  :  S → R
 --        fun→  :  R → S
---        fiso← : (x : R)  → fun← ( fun→ x )  ≡ x 
---        fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x 
--- 
+--        fiso← : (x : R)  → fun← ( fun→ x )  ≡ x
+--        fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x
+--
 -- injection :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
 -- injection R S f = (x y : R) → f x ≡ f y → x ≡ y
 
-open Bijection 
+open Bijection
 
 bi-trans : {n m l : Level} (R : Set n) (S : Set m) (T : Set l)  → Bijection R S → Bijection S T → Bijection R T
 bi-trans R S T rs st = record { fun← = λ x → fun← rs ( fun← st x ) ; fun→ = λ x → fun→ st ( fun→ rs x )
@@ -36,17 +36,17 @@
     ; fiso→ = λ x →  trans (cong (λ k → fun→ st k) (fiso→ rs (fun← st x))) ( fiso→ st x) }
 
 bid : {n : Level} (R : Set n)  → Bijection R R
-bid {n} R = record {  fun← = λ x → x ; fun→  = λ x → x ; fiso← = λ _ → refl ;  fiso→ = λ _ → refl } 
+bid {n} R = record {  fun← = λ x → x ; fun→  = λ x → x ; fiso← = λ _ → refl ;  fiso→ = λ _ → refl }
 
 bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S →  Bijection S R
-bi-sym R S eq = record {  fun← =  fun→ eq ; fun→  = fun← eq  ; fiso← =  fiso→ eq ;  fiso→ =  fiso← eq } 
+bi-sym R S eq = record {  fun← =  fun→ eq ; fun→  = fun← eq  ; fiso← =  fiso→ eq ;  fiso→ =  fiso← eq }
 
 open import Relation.Binary.Structures
 
 bijIsEquivalence : {n : Level } → IsEquivalence  (Bijection {n} {n})
 bijIsEquivalence = record { refl = λ {R} → bid R ; sym = λ {R} {S} → bi-sym R S ; trans = λ {R} {S} {T} → bi-trans R S T }
 
---  ¬ A = A → ⊥ 
+--  ¬ A = A → ⊥
 --
 -- famous diagnostic function
 --
@@ -56,7 +56,7 @@
 
 diagonal : { S : Set } → ¬ Bijection  ( S → Bool ) S
 diagonal {S} b = diagn1 (fun→ b (λ n → diag b n) ) refl where
-    diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n ) 
+    diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n )
     diagn1 n dn = ¬t=f (diag b n ) ( begin
            not (diag b n)
         ≡⟨⟩
@@ -66,10 +66,10 @@
         ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
            not (fun← b n n)
         ≡⟨⟩
-           diag b n 
+           diag b n
         ∎ ) where open ≡-Reasoning
 
-b1 : (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ 
+b1 : (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ
 b1 b = fun→ b (diag b)
 
 b-iso : (b : Bijection  ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b)
@@ -105,7 +105,7 @@
   field
      j k : ℕ
      k1 : nxn→n j k ≡ i
-     nn-unique : {j0 k0 : ℕ } →  nxn→n j0 k0 ≡ i  → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ 
+     nn-unique : {j0 k0 : ℕ } →  nxn→n j0 k0 ≡ i  → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫
 
 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0
 i≤0→i≡0 {0} z≤n = refl
@@ -114,7 +114,7 @@
 nxn : Bijection ℕ (ℕ ∧ ℕ)
 nxn = record {
      fun← = λ p → nxn→n (proj1 p) (proj2 p)
-   ; fun→ =  n→nxn 
+   ; fun→ =  n→nxn
    ; fiso← = λ i → NN.k1 (nn i)
    ; fiso→ = λ x → nn-id (proj1 x) (proj2 x)
   } where
@@ -123,10 +123,10 @@
      nxn→n zero (suc j) = j + suc (nxn→n zero j)
      nxn→n (suc i) zero = suc i + suc (nxn→n i zero)
      nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j))
-     nn : ( i  : ℕ) → NN i nxn→n 
+     nn : ( i  : ℕ) → NN i nxn→n
      n→nxn : ℕ → ℕ ∧ ℕ
      n→nxn n = ⟪ NN.j (nn n)  , NN.k (nn n) ⟫
-     k0 : {i : ℕ } → n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ 
+     k0 : {i : ℕ } → n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫
      k0 {i} = refl
 
      nxn→n0 : { j k : ℕ } →  nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 )
@@ -156,7 +156,7 @@
      nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
 
      -- increment in the same stage
-     nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
+     nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j
      nid2 zero zero = refl
      nid2 zero (suc j) = refl
      nid2 (suc i) zero = begin
@@ -181,7 +181,7 @@
              open ≡-Reasoning
 
      -- increment the stage
-     nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) 
+     nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i)
      nid00 zero = refl
      nid00 (suc i) = begin
         suc (suc (i + suc (nxn→n i 0))) ≡⟨ cong (λ k → suc (suc (i + k ))) (nid00 i) ⟩
@@ -195,10 +195,10 @@
      --
      -- create the invariant NN for all n
      --
-     nn zero = record { j = 0 ; k = 0 ; k1 = refl 
+     nn zero = record { j = 0 ; k = 0 ; k1 = refl
         ;  nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
-     nn (suc i) with NN.k (nn i)  | inspect  NN.k (nn i) 
-     ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 
+     nn (suc i) with NN.k (nn i)  | inspect  NN.k (nn i)
+     ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0
          ; k1 = nn02 ; nn-unique = nn04 } where
             ---
             --- increment the stage
@@ -219,28 +219,28 @@
                suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩
                suc i ∎  where open ≡-Reasoning
             nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (sum ) ⟫ ≡ ⟪ j0 , k0 ⟫
-            nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i -- 
+            nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i --
                nn07 : nxn→n k0 0 ≡ i
                nn07 = cong pred ( begin
                   suc ( nxn→n k0 0 ) ≡⟨ nid00 k0 ⟩
                   nxn→n 0 (suc k0 )  ≡⟨ eq1 ⟩
-                  suc i  ∎ )  where open ≡-Reasoning 
-               nn08 : k0 ≡ sum 
+                  suc i  ∎ )  where open ≡-Reasoning
+               nn08 : k0 ≡ sum
                nn08 = begin
                   k0  ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩
                   NN.j (nn i)  ≡⟨ +-comm 0 _ ⟩
                   NN.j (nn i) + 0  ≡⟨ cong (λ k →  NN.j (nn i) + k) (sym eq) ⟩
                   NN.j (nn i) + NN.k (nn i)  ≡⟨ NNnn  ⟩
-                  sum   ∎   where open ≡-Reasoning 
+                  sum   ∎   where open ≡-Reasoning
             nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where
                nn05 : nxn→n j0 (suc k0) ≡ i
                nn05 = begin
-                  nxn→n j0 (suc k0)  ≡⟨ cong pred ( begin 
+                  nxn→n j0 (suc k0)  ≡⟨ cong pred ( begin
                     suc (nxn→n j0 (suc k0))  ≡⟨ nid2 j0 k0 ⟩
                     nxn→n (suc j0) k0  ≡⟨ eq1 ⟩
                     suc i ∎ ) ⟩
-                  i ∎   where open ≡-Reasoning 
-               nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ 
+                  i ∎   where open ≡-Reasoning
+               nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫
                nn06 = NN.nn-unique (nn i)
      ... | suc k  | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ;  nn-unique = nn13 } where
             ---
@@ -251,23 +251,23 @@
             j = NN.j (nn i)
             NNnn :  NN.j (nn i) + NN.k (nn i) ≡ sum
             NNnn = sym refl
-            nn10 : suc (NN.j (nn i)) + k ≡ sum 
+            nn10 : suc (NN.j (nn i)) + k ≡ sum
             nn10 = begin
                 suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _)  ⟩
                 (NN.j (nn i) + 1) + k ≡⟨  +-assoc (NN.j (nn i)) 1 k ⟩
                 NN.j (nn i) + suc k  ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩
                 NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn  ⟩
-                sum   ∎   where open ≡-Reasoning 
+                sum   ∎   where open ≡-Reasoning
             nn11 :  nxn→n (suc (NN.j (nn i))) k ≡ suc i --  nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i
             nn11 = begin
                 nxn→n (suc (NN.j (nn i))) k   ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩
                 suc (nxn→n (NN.j (nn i)) (suc k)) ≡⟨ cong (λ k →   suc (nxn→n (NN.j (nn i)) k)) (sym eq) ⟩
                 suc (nxn→n ( NN.j (nn i)) (NN.k (nn i)))  ≡⟨ cong suc (NN.k1 (nn i)) ⟩
-                suc i  ∎   where open ≡-Reasoning 
+                suc i  ∎   where open ≡-Reasoning
             nn18 :  zero < NN.k (nn i)
             nn18 = subst (λ k → 0 < k ) ( begin
                     suc k ≡⟨ sym eq ⟩
-                    NN.k (nn i)  ∎  ) (s≤s z≤n )  where open ≡-Reasoning  
+                    NN.k (nn i)  ∎  ) (s≤s z≤n )  where open ≡-Reasoning
             nn13 :  {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ suc (NN.j (nn i)) , k ⟫ ≡ ⟪ j0 , k0 ⟫
             nn13 {zero} {suc k0} eq1 = ⊥-elim ( nat-≡< (sym (cong proj2 nn17)) nn18 ) where  -- (nxn→n zero (suc k0)) ≡ suc i
                 nn16 : nxn→n k0 zero ≡ i
@@ -276,7 +276,7 @@
                 nn17 = NN.nn-unique (nn i) nn16
             nn13 {suc j0} {k0} eq1 = begin
                ⟪ suc (NN.j (nn i)) , pred (suc k) ⟫ ≡⟨ cong (λ k →  ⟪ suc (NN.j (nn i)) , pred k ⟫ ) (sym eq) ⟩
-               ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin 
+               ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin
                  ⟪ NN.j (nn i) , NN.k (nn i) ⟫  ≡⟨ nn15 ⟩
                  ⟪ j0 , suc k0 ⟫ ∎ ) ⟩
                ⟪ suc j0 , k0 ⟫ ∎  where -- nxn→n (suc j0) k0 ≡ suc i
@@ -307,24 +307,24 @@
   field
      nlist : List Bool
      isBin : lton nlist ≡ n
-     isUnique :  (x : List Bool) → lton x ≡ n → nlist  ≡ x 
+     isUnique :  (x : List Bool) → lton x ≡ n → nlist  ≡ x
 
 lb+1 : List Bool → List Bool
-lb+1 [] =  false ∷ [] 
-lb+1 (false ∷ t) = true ∷ t 
+lb+1 [] =  false ∷ []
+lb+1 (false ∷ t) = true ∷ t
 lb+1 (true ∷ t) =  false ∷ lb+1 t
 
 lb-1 : List Bool → List Bool
 lb-1 [] =  []
-lb-1 (true ∷ t) = false ∷ t 
+lb-1 (true ∷ t) = false ∷ t
 lb-1 (false ∷ t) with lb-1 t
 ... | [] = true ∷ []
 ... | x ∷ t1 = true ∷ x ∷ t1
 
-LBℕ : Bijection ℕ ( List Bool ) 
+LBℕ : Bijection ℕ ( List Bool )
 LBℕ = record {
-       fun←  = λ x → lton x 
-     ; fun→  = λ n → LB.nlist (lb n) 
+       fun←  = λ x → lton x
+     ; fun→  = λ n → LB.nlist (lb n)
      ; fiso← = λ n → LB.isBin (lb n)
      ; fiso→ = λ x → LB.isUnique (lb (lton x)) x refl
    } where
@@ -335,7 +335,7 @@
      lton : List Bool → ℕ
      lton x  = pred (lton1 x)
 
-     lton1>0 : (x : List Bool ) → 0 < lton1 x 
+     lton1>0 : (x : List Bool ) → 0 < lton1 x
      lton1>0 [] = a<sa
      lton1>0 (true ∷ x₁) = 0<s
      lton1>0 (false ∷ t) = ≤-trans (lton1>0 t) x≤x+y
@@ -364,7 +364,7 @@
      lb=2 : {x y : ℕ } → pred x  < pred y → suc (x + x ) < suc (y + y )
      lb=2 {zero} {suc y} lt = s≤s 0<s
      lb=2 {suc x} {suc y} lt = s≤s (lb=0 {suc x} {suc y} lt)
-     lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y 
+     lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y
      lb=1 {x} {y} {true} eq with <-cmp (lton x) (lton y)
      ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=2 {lton1 x} {lton1 y} a))
      ... | tri≈ ¬a b ¬c = b
@@ -391,7 +391,7 @@
             (y + y) ∸ 1  ∎  where open ≤-Reasoning
      ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (lb=02 c) ) where
         lb=02 : {x y : ℕ } → x  < y → x + x ∸ 1 < y + y
-        lb=02 {0} {y} lt = ≤-trans lt x≤x+y 
+        lb=02 {0} {y} lt = ≤-trans lt x≤x+y
         lb=02 {suc x} {y} lt = begin
             suc ( suc x + suc x ∸ 1 ) ≡⟨ refl ⟩
             suc x + suc x  ≤⟨ ≤-plus {suc x} (<to≤ lt) ⟩
@@ -411,54 +411,54 @@
      lb=b (x ∷ y) [] eq = ⊥-elim ( nat-≡< (sym eq) (lton-cons>0 {x} {y} ))
      lb=b (true ∷ x) (false ∷ y) eq = ⊥-elim ( lb-tf {x} {y} eq )
      lb=b (false ∷ x) (true ∷ y) eq = ⊥-elim ( lb-tf {y} {x} (sym eq) )
-     lb=b (true ∷ x)  (true ∷ y)  eq = cong (λ k → true ∷ k  ) (lb=b x y (lb=1 {x} {y} {true}  eq)) 
-     lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq)) 
+     lb=b (true ∷ x)  (true ∷ y)  eq = cong (λ k → true ∷ k  ) (lb=b x y (lb=1 {x} {y} {true}  eq))
+     lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq))
 
      lb : (n : ℕ) → LB n lton
      lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where
          lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x
          lb05 x eq = lb=b [] x (sym eq)
-     lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) 
+     lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n)
      ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where
          open ≡-Reasoning
          lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n
          lb10 = begin
-           lton (false ∷ []) ≡⟨ refl ⟩ 
-           suc 0  ≡⟨ refl ⟩ 
-           suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ 
-           suc (lton (LB.nlist (lb n)))  ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ 
-           suc n ∎    
+           lton (false ∷ []) ≡⟨ refl ⟩
+           suc 0  ≡⟨ refl ⟩
+           suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩
+           suc (lton (LB.nlist (lb n)))  ≡⟨ cong suc (LB.isBin (lb n) ) ⟩
+           suc n ∎
          lb06 :  (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x
          lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x
      ... | false ∷ t | record { eq = eq } =  record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
-           lton (true ∷ t)  ≡⟨ refl ⟩ 
-           lton1 t + lton1 t   ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩ 
-           suc (pred (lton1 t + lton1 t ))  ≡⟨ refl ⟩ 
-           suc (lton (false ∷ t))   ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩ 
-           suc (lton (LB.nlist (lb n))) ≡⟨  cong suc (LB.isBin (lb n)) ⟩ 
+           lton (true ∷ t)  ≡⟨ refl ⟩
+           lton1 t + lton1 t   ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩
+           suc (pred (lton1 t + lton1 t ))  ≡⟨ refl ⟩
+           suc (lton (false ∷ t))   ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩
+           suc (lton (LB.nlist (lb n))) ≡⟨  cong suc (LB.isBin (lb n)) ⟩
            suc n ∎  where open ≡-Reasoning
         lb09 :  (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x
         lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) --  lton (true ∷ t) ≡ lton x
      ... | true ∷ t | record { eq = eq } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where
         lb03 : lton (true ∷ t) ≡ n
         lb03 = begin
-           lton (true ∷ t)   ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ 
-           lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩ 
+           lton (true ∷ t)   ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩
+           lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩
            n ∎  where open ≡-Reasoning
 
         add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc  (x1 + x1))
         add11 zero = refl
         add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x)))
 
-        lb04 : (t : List Bool) →  suc (lton1 t) ≡ lton1 (lb+1 t) 
+        lb04 : (t : List Bool) →  suc (lton1 t) ≡ lton1 (lb+1 t)
         lb04 [] = refl
         lb04 (false ∷ t) = refl
         lb04 (true ∷ []) = refl
         lb04 (true ∷ t0 )  = begin
-           suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩ 
-           suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0  ) ⟩ 
+           suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩
+           suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0  ) ⟩
            lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎  where
               open ≡-Reasoning
 
@@ -473,7 +473,7 @@
             suc n ∎  where open ≡-Reasoning
 
         lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x
-        lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1)) 
+        lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1))
 
 -- Bernstein is non constructive, so we cannot use this without some assumption
 --   but in case of ℕ, we can construct it directly.
@@ -488,8 +488,8 @@
       a : A
       fa=c : f a ≡ c
 
-Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ 
-     → (fi : InjectiveF A  B ) → (gi : InjectiveF  B C )  
+Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ
+     → (fi : InjectiveF A  B ) → (gi : InjectiveF  B C )
      → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c)  )
      → Bijection B ℕ
 Countable-Bernstein A B C an cn fi gi is-A is-B = record {
@@ -514,8 +514,8 @@
     record CB (n : ℕ) : Set where
       field
          ca cb : ℕ
-         cb≤n  : cb ≤ suc n  
-         ca≤cb : ca ≤ cb  
+         cb≤n  : cb ≤ suc n
+         ca≤cb : ca ≤ cb
          na : {i : ℕ} → i < ca → A
          nb : {i : ℕ} → i < cb → B
 
@@ -529,49 +529,75 @@
 
     lb : (n : ℕ ) → CB n
     lb zero with is-A (fun← cn zero) | is-B (fun← cn zero)
-    ... | yes isA | yes isB =  record { ca = suc zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ≤-refl ; na = λ _ → Is.a isA ; nb = λ _ → Is.a isB } 
+    ... | yes isA | yes isB =  record { ca = suc zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ≤-refl ; na = λ _ → Is.a isA ; nb = λ _ → Is.a isB }
     ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB = record { ca = zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = px≤x  ; na = λ () ; nb = λ _ → Is.a isB } 
-    ... | no nisA | no nisB = record { ca = zero ; cb = zero ; cb≤n = px≤x ; ca≤cb = ≤-refl ; na = λ () ; nb = λ () } 
+    ... | no nisA | yes isB = record { ca = zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = px≤x  ; na = λ () ; nb = λ _ → Is.a isB }
+    ... | no nisA | no nisB = record { ca = zero ; cb = zero ; cb≤n = px≤x ; ca≤cb = ≤-refl ; na = λ () ; nb = λ () }
     lb (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n))
-    ... | yes isA | yes isB =  record { ca = suc (CB.ca (lb n)) ; cb = suc (CB.cb (lb n)) ; cb≤n = s≤s (CB.cb≤n (lb n)) ; ca≤cb = s≤s (CB.ca≤cb (lb n)) 
+    ... | yes isA | yes isB =  record { ca = suc (CB.ca (lb n)) ; cb = suc (CB.cb (lb n)) ; cb≤n = s≤s (CB.cb≤n (lb n)) ; ca≤cb = s≤s (CB.ca≤cb (lb n))
         ; na = na ; nb = nb } where
            na : {i : ℕ} → i < suc (CB.ca (lb n)) → A
            na {i} i<a with <-∨ i<a
-           ... | case1 refl = Is.a isA 
+           ... | case1 refl = Is.a isA
            ... | case2 i<a = CB.na (lb n) i<a
            nb : {i : ℕ} → i < suc (CB.cb (lb n)) → B
            nb {i} i<a with <-∨ i<a
-           ... | case1 refl = Is.a isB 
+           ... | case1 refl = Is.a isB
            ... | case2 i<a = CB.nb (lb n) i<a
     ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB = record { ca = CB.ca (lb n) ; cb = suc (CB.cb (lb n)) ; cb≤n = s≤s (CB.cb≤n (lb n)) ; ca≤cb = ≤-trans (CB.ca≤cb (lb n)) px≤x 
+    ... | no nisA | yes isB = record { ca = CB.ca (lb n) ; cb = suc (CB.cb (lb n)) ; cb≤n = s≤s (CB.cb≤n (lb n)) ; ca≤cb = ≤-trans (CB.ca≤cb (lb n)) px≤x
         ; na = CB.na (lb n)  ; nb = nb } where
            nb : {i : ℕ} → i < suc (CB.cb (lb n)) → B
            nb {i} i<a with <-∨ i<a
-           ... | case1 refl = Is.a isB 
+           ... | case1 refl = Is.a isB
            ... | case2 i<a = CB.nb (lb n) i<a
-    ... | no nisA | no nisB = record { ca = CB.ca (lb n) ; cb = CB.cb (lb n) ; cb≤n = ≤-trans (CB.cb≤n (lb n)) px≤x  ; ca≤cb =  CB.ca≤cb (lb n) 
-        ; na = CB.na (lb n) ; nb = CB.nb (lb n) } 
+    ... | no nisA | no nisB = record { ca = CB.ca (lb n) ; cb = CB.cb (lb n) ; cb≤n = ≤-trans (CB.cb≤n (lb n)) px≤x  ; ca≤cb =  CB.ca≤cb (lb n)
+        ; na = CB.na (lb n) ; nb = CB.nb (lb n) }
 
     cbn : ℕ → ℕ
     cbn n = fun→ cn (g (f (fun← an n)))
 
+    cbn-mono1 : {i : ℕ} → cbn i < cbn (suc i)
+    cbn-mono1 {i} with cbn i | inspect cbn i | lb (cbn i) 
+    ... | zero | record {eq = eq1 } | s with is-A (fun← cn (cbn i)) | is-B (fun← cn (cbn i))
+    ... | yes isA | yes isB = ?
+    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB = ⊥-elim ( nisA record { a = fun← an i ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl  )   } )
+    ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an i ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl  )   } )
+    cbn-mono1 {i} | suc t | record {eq = eq1 } | s with is-A (fun← cn (suc t)) | is-B (fun← cn (suc t))
+    ... | yes isA | yes isB = ? -- <-transʳ z≤n ≤-refl 
+    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB = ⊥-elim ( nisA record { a = fun← an i ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  eq1 )   } )
+    ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an i ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  eq1 )   } )
+
+    cbn-mono : {i j : ℕ} → i < j → cbn i < cbn j
+    cbn-mono {i} {suc j} (s≤s i≤j) with <-∨ {i} {j} (<-transʳ i≤j a<sa )
+    ... | case1 refl = cbn-mono1
+    ... | case2 lt = <-trans (cbn-mono {i} {j} lt) cbn-mono1
+
     cb< : (n : ℕ) → CB.cb (lb (cbn n)) < CB.cb (lb (cbn (suc n)))
-    cb< = ?
-          
+    cb< n = cb00 _ _ _ refl refl   where
+        cb00 : (n i j : ℕ) → i ≡ cbn n → j ≡ cbn (suc n)  → CB.cb (lb i) < CB.cb (lb j)
+        cb00 zero i j eq eq1 = ?
+        cb00 (suc n) i j eq eq1 = <-trans (cb00 n i j ? ?  ) ?
+
+    cb<0 : 0 < CB.cb (lb (cbn 0))
+    cb<0 with cbn 0 | inspect cbn 0
+    ... | zero | record { eq = eq1 } with is-A (fun← cn zero) | is-B (fun← cn zero)
+    ... | yes isA | yes isB =  ≤-refl
+    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB = ≤-refl
+    ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  eq1)   } )
+    cb<0 | suc t | record { eq = eq1 } with is-A (fun← cn (suc t)) | is-B (fun← cn (suc t))
+    ... | yes isA | yes isB = <-transʳ z≤n ≤-refl 
+    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB = <-transʳ z≤n ≤-refl 
+    ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  eq1 )   } )
+
     n<cbn : (n : ℕ) →  n < CB.cb (lb (cbn n))
-    n<cbn zero with is-A (fun← cn zero) | is-B (fun← cn zero) | inspect lb zero
-    ... | yes isA | yes isB | record { eq = eq1 } = subst (λ k → 1 ≤ CB.cb (lb k)) lem02 lem01  where
-         lem01 :  1 ≤ CB.cb (lb 0)
-         lem01 = subst (λ k → 1 ≤ k ) (sym (cong CB.cb eq1))  ≤-refl
-         lem02 : 0 ≡ fun→ cn (g (f (fun← an 0)))
-         lem02 = ?
-    ... | yes isA | no nisB | record { eq = eq1 } = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB | record { eq = eq1 } = ?
-    ... | no nisA | no nisB | record { eq = eq1 } = ?
+    n<cbn zero = cb<0
     n<cbn (suc n) = begin
-       suc (suc n)  ≤⟨ s≤s (n<cbn n) ⟩  
+       suc (suc n)  ≤⟨ s≤s (n<cbn n) ⟩
        suc (CB.cb (lb (cbn n)))  ≤⟨ cb< n ⟩
        CB.cb (lb (cbn (suc n)))  ∎  where
           open ≤-Reasoning
@@ -587,12 +613,12 @@
      ; fun→  = λ n → ⟪ fun→  ab (proj1 n) , fun→  cd (proj2 n) ⟫
      ; fiso← = lem0
      ; fiso→ = lem1
-  } where 
-      open Bijection 
+  } where
+      open Bijection
       lem0 : (x : A ∧ C) → ⟪ fun← ab (fun→ ab (proj1 x)) , fun← cd (fun→ cd (proj2 x)) ⟫ ≡ x
-      lem0 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso← ab x) (fiso← cd y)   
+      lem0 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso← ab x) (fiso← cd y)
       lem1 : (x : B ∧ D) → ⟪ fun→ ab (fun← ab (proj1 x)) , fun→ cd (fun← cd (proj2 x)) ⟫ ≡ x
-      lem1 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso→ ab x) (fiso→ cd y)   
+      lem1 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso→ ab x) (fiso→ cd y)
 
 
 LM1 : (A : Set ) → Bijection (List A ) ℕ → Bijection (List A ∧ List Bool) ℕ
@@ -605,7 +631,7 @@
 LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln)  fi gi ? ? where
    f : List A → List (Maybe A)
    f [] = []
-   f (x ∷ t) = just x ∷ f t 
+   f (x ∷ t) = just x ∷ f t
    f-inject : {x y : List A} → f x ≡ f y → x ≡ y
    f-inject {[]} {[]} refl = refl
    f-inject {x ∷ xt} {y ∷ yt} eq = cong₂ (λ j k → j ∷ k ) (just-injective (∷-injectiveˡ eq)) (f-inject (∷-injectiveʳ eq) )
@@ -613,20 +639,20 @@
    g [] = ⟪ [] , [] ⟫
    g (just h ∷ t)  = ⟪ h ∷ proj1 (g t) , true  ∷ proj2 (g t) ⟫
    g (nothing ∷ t) = ⟪     proj1 (g t) , false ∷ proj2 (g t) ⟫
-   g⁻¹ :  List A ∧ List Bool → List (Maybe A) 
+   g⁻¹ :  List A ∧ List Bool → List (Maybe A)
    g⁻¹ ⟪ [] , [] ⟫ = []
-   g⁻¹ ⟪ x ∷ xt , [] ⟫ = just x ∷  g⁻¹ ⟪ xt , [] ⟫ 
+   g⁻¹ ⟪ x ∷ xt , [] ⟫ = just x ∷  g⁻¹ ⟪ xt , [] ⟫
    g⁻¹ ⟪ [] , true ∷ y ⟫ = []
    g⁻¹ ⟪ x ∷ xt , true ∷ yt ⟫ = just x ∷ g⁻¹ ⟪ xt , yt ⟫
-   g⁻¹ ⟪ [] , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ [] , y ⟫  
+   g⁻¹ ⟪ [] , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ [] , y ⟫
    g⁻¹ ⟪ x ∷ x₁ , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ x ∷ x₁ , y ⟫
    g-iso : {x : List (Maybe A)} → g⁻¹ (g x) ≡ x
    g-iso {[]} = refl
    g-iso {just x ∷ xt} = cong ( λ k → just x ∷ k) ( g-iso )
    g-iso {nothing ∷ []} = refl
    g-iso {nothing ∷ just x ∷ xt} = cong (λ k → nothing ∷ k ) ( g-iso {_} )
-   g-iso {nothing ∷ nothing ∷ xt} with g-iso {nothing ∷ xt} 
-   ... | t = trans (lemma01 (proj1 (g xt)) (proj2 (g xt)) ) ( cong (λ k → nothing ∷ k ) t ) where 
+   g-iso {nothing ∷ nothing ∷ xt} with g-iso {nothing ∷ xt}
+   ... | t = trans (lemma01 (proj1 (g xt)) (proj2 (g xt)) ) ( cong (λ k → nothing ∷ k ) t ) where
          lemma01 : (x : List A) (y : List Bool ) →  g⁻¹ ⟪ x , false ∷ false ∷ y ⟫ ≡ nothing ∷ g⁻¹ ⟪ x , false ∷ y ⟫
          lemma01 [] y = refl
          lemma01 (x ∷ x₁) y = refl
@@ -639,9 +665,9 @@
 
 -- open import Data.Fin
 --
---- LBFin : {n : ℕ } → Bijection (List (Meybe (Fin n))) ( List (Fin (suc n))) 
+--- LBFin : {n : ℕ } → Bijection (List (Meybe (Fin n))) ( List (Fin (suc n)))
 --
---- LBFin : {n : ℕ } → Bijection ℕ ( List (Fin n)) 
+--- LBFin : {n : ℕ } → Bijection ℕ ( List (Fin n))
 --- LBFin = ?
 
 --