# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686297291 -32400
# Node ID a93764db7c6789f4c91f53e543df67dd4ff047f2
# Parent  f4bd059227f83a80fd3663d1c18d71aaf16cd1b9
...

diff -r f4bd059227f8 -r a93764db7c67 src/bijection.agda
--- a/src/bijection.agda	Fri Jun 09 11:26:36 2023 +0900
+++ b/src/bijection.agda	Fri Jun 09 16:54:51 2023 +0900
@@ -456,7 +456,7 @@
         lb04 [] = refl
         lb04 (false ∷ t) = refl
         lb04 (true ∷ []) = refl
-        lb04 (true ∷ t0 )  = begin
+        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  ) ⟩
            lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎  where
@@ -464,7 +464,7 @@
 
         lb02 : (t : List Bool) → lton t ≡ n → lton (lb+1 t) ≡ suc n
         lb02 [] refl = refl
-        lb02 t eq1 = begin
+        lb02 (t @ (_ ∷ _)) eq1 = begin
             lton (lb+1 t) ≡⟨ refl ⟩
             pred (lton1 (lb+1 t)) ≡⟨ cong pred (sym (lb04 t)) ⟩
             pred (suc (lton1 t))  ≡⟨ sym (sucprd (lton1>0 t)) ⟩
@@ -511,13 +511,25 @@
     --     the count of B is the numner of B in Bijection B ℕ
     --     if we have a , number a of A is larger than the numner of B C, so we have the inverse
     --
-    record CB (n : ℕ) : Set where
-      field
-         ca cb : ℕ
-         cb≤n  : cb ≤ suc n
-         ca≤cb : ca ≤ cb
-         na : {i : ℕ} → i < ca → A
-         nb : {i : ℕ} → i < cb → B
+
+    count-B : ℕ → ℕ 
+    count-B zero with is-B (fun← cn zero)
+    ... | yes isb = 1
+    ... | no nisb = 0
+    count-B (suc n) with is-B (fun← cn (suc n))
+    ... | yes isb = suc (count-B n)
+    ... | no nisb = count-B n
+
+    bton : B → ℕ
+    bton b = count-B (fun→ cn (g b))
+
+    count-A : ℕ → ℕ 
+    count-A zero with is-A (fun← cn zero)
+    ... | yes isb = 1
+    ... | no nisb = 0
+    count-A (suc n) with is-A (fun← cn (suc n))
+    ... | yes isb = suc (count-A n)
+    ... | no nisb = count-A n
 
     ¬isA∧isB : (y : C ) →  Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥
     ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where
@@ -527,76 +539,40 @@
            y ∎ where
              open ≡-Reasoning
 
-    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 }
+    ca≤cb0 : (n : ℕ) → count-A n ≤ count-B n
+    ca≤cb0 zero 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 = 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))
-        ; 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
-           ... | 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
-           ... | case2 i<a = CB.nb (lb n) i<a
+    ... | no nisA | yes isB = px≤x  
+    ... | no nisA | no nisB = ≤-refl 
+    ca≤cb0 (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n))
+    ... | yes isA | yes isB = s≤s (ca≤cb0 n)
     ... | 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
-        ; 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
-           ... | 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 | yes isB = ≤-trans (ca≤cb0 n) px≤x
+    ... | no nisA | no nisB = ca≤cb0 n
 
-    --   cb = count of B  monotonic    i ≤ j → CB.cb i ≤ CB.cb j ≤ j
-    --   ca = count of A  monotonic    i ≤ j → CB.ca i ≤ CB.ca j ≤ j
-    --      ca ≤ cb from CB 
-    --   cbn i : i ≡ fun← an n → i count of different B → some b ≥ i  
-    --   cbn 0     0 ≤ CB.cb (fun→ cn (g (f (fun→ an 0))))
-    --   cbn (suc i)     i < cbn i → cbn i 
-    --                   cbn i ≤ i → it contains all b ≤ i → f (fun← an n) is not in this → i < f (fun← an n) 
-
-    record CBN ( n : ℕ ) : Set where
-       field
-           cbn : ℕ
-           n<cbn : n < CB.cb (lb cbn )
-
-    cbn : (n : ℕ ) → CBN n
-    cbn 0 = record { cbn = j ; n<cbn = cb<0 _ refl  }  where
-        j =  CB.cb (lb (fun→ cn (g (f (fun← an zero))))) 
-        cb<0 : (i : ℕ) → i ≡ CB.cb (lb j) → 0 < i
-        cb<0 0 eq with is-A (fun← cn zero) | is-B (fun← cn zero)
-        ... | yes isA | yes isB = ?
-        ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-        ... | no nisA | yes isB = ?
-        ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  ? )   } )
-        cb<0 (suc i) eq = 0<s
-    cbn (suc n) with <∨≤ (suc n) (CB.cb (lb (CBN.cbn (cbn n))))
-    ... | case1 lt = record { cbn = CBN.cbn (cbn n) ; n<cbn = lt }
-    ... | case2 le = ?
-
-    bton : B → ℕ
-    bton b = CB.cb (lb (fun→ cn (g b)))
-    ntob : ℕ → B
-    ntob n = CB.nb (lb (CBN.cbn (cbn n))) (CBN.n<cbn (cbn n))
+    ntob : (n : ℕ) → B
+    ntob n = lem01 (fun→ cn (g (f (fun← an n)))) (≤-trans (lem02 _ refl ) (ca≤cb0 (fun→ cn (g (f (fun← an n)))))) where
+        lem02 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an n))) → 1 ≤ count-A i
+        lem02 zero eq with is-A (fun← cn zero)
+        ... | yes isA = ≤-refl
+        ... | no nisA = ⊥-elim (nisA record { a = (fun← an n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
+        lem02 (suc i) eq with is-A (fun← cn (suc i))
+        ... | yes isA = s≤s z≤n
+        ... | no nisA = ⊥-elim (nisA record { a = (fun← an n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq))  })
+        lem01 : (i : ℕ) → zero < count-B i → B
+        lem01 zero lt with is-B (fun← cn zero)
+        ... | yes isB = Is.a isB
+        ... | no nisB = ⊥-elim (¬a≤a lt)
+        lem01 (suc i) lt with is-B (fun← cn (suc i))
+        ... | yes isB = Is.a isB
+        ... | no nisB = lem01 i lt 
 
     biso : (n : ℕ) → bton (ntob n) ≡ n
-    biso n = lem00 n where
-        lem00 : (n : ℕ) → CB.cb (lb (fun→ cn (g (CB.nb (lb (CBN.cbn (cbn n))) (CBN.n<cbn (cbn n)))))) ≡ n
-        lem00 zero = ?
-        lem00 (suc n) = ?
+    biso n = ?
 
     biso1 : (b : B) → ntob (bton b) ≡ b
-    biso1 b = lem01 _ _ b (CBN.n<cbn (cbn (CB.cb (lb (fun→ cn (g b)))))) refl where
-        lem01 : (i j : ℕ) → (b : B) → (lt : j < CB.cb (lb i)) → i ≡ (CBN.cbn (cbn (CB.cb (lb (fun→ cn (g b)))))) → CB.nb (lb i) lt ≡ b
-        lem01 zero j b lt eq = ?
-        lem01 (suc i) j b lt eq = ?
+    biso1 b = ?
 
 bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D)
 bi-∧ {A} {B} {C} {D} ab cd = record {