# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687538664 -32400
# Node ID 0d29328c0441d1946f2bc0ce9a66aa906982dc3a
# Parent  51abc18e6f17c727f8f7899d2db3b7627f867521
...

diff -r 51abc18e6f17 -r 0d29328c0441 src/bijection.agda
--- a/src/bijection.agda	Fri Jun 23 15:36:09 2023 +0900
+++ b/src/bijection.agda	Sat Jun 24 01:44:24 2023 +0900
@@ -708,24 +708,6 @@
             ca-list cl ∎ where
                 open ≤-Reasoning
 
-    anygb : (b : B) → Any (_≡_ (g b)) (clist (c (fun→ cn (g b))))
-    anygb = ?
-
-    bton1 : B → ℕ
-    bton1 b = bton10 b (clist (c (fun→ cn (g b)))) ? where
-        bton10 : (b : B) → (x : List C) →  Any (_≡_ (g b)) x → ℕ
-        bton10 b (h ∷ t) (here px)  = count-B ( fun→ cn h )
-        bton10 b (h ∷ t) (there ax) = bton10 b t ax
-
-    anycb : (n : ℕ) → Any (λ c₁ → Is B C g c₁ ∧ (count-B (fun→ cn c₁) ≡ n)) (clist (c n))
-    anycb = ?
-
-    ntob1 : (n : ℕ) → B
-    ntob1 n = bton10 n (clist (c n)) ? where
-        bton10 : (n : ℕ) → (x : List C) → Any (λ c → Is B C g c ∧ (count-B (fun→ cn c) ≡ n)) x →  B
-        bton10 n (h ∷ t) (here px) = Is.a (proj1 px)
-        bton10 n (h ∷ t) (there ax) = bton10 n t ax
-
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ
@@ -740,32 +722,76 @@
           cb : ℕ
           b=cn : fun← cn cb ≡ g b
           cb=n : count-B cb ≡ suc n
-          cb-inject : (cb1 : ℕ) → count-B cb ≡ count-B cb1 → cb ≡ cb1
+          cb-inject : (cb1 : ℕ) → Is B C g (fun← cn cb1) → count-B cb ≡ count-B cb1 → cb ≡ cb1
+
+    count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j
+    count-B-mono {i} {j} i≤j with ≤-∨ i≤j
+    ... | case1 refl = ≤-refl
+    ... | case2 i<j = lem00 _ _ i<j where
+         lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j
+         lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where
+             lem01 : (j : ℕ) → count-B j ≤ count-B (suc j)
+             lem01 zero with is-B (fun← cn (suc zero))
+             ... | yes isb = refl-≤s
+             ... | no nisb = ≤-refl
+             lem01 (suc n) with is-B (fun← cn (suc (suc n)))
+             ... | yes isb = refl-≤s
+             ... | no nisb = ≤-refl
 
     lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
     lem01 n i le = lem09 i (count-B i) le refl where
         -- starting from 0, if count B i ≡ suc n, this is it
+
+        lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B i ≡ count-B j → i ≡ j
+        lem06 i j bi bj eq = lem08  where
+            lem20 : (i j : ℕ) → i < j →  Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥
+            lem20 zero j i<j bi bj le = ?
+            lem20 (suc i) zero () bi bj le
+            lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ? where
+                 --
+                 --                    i  <     suc i  ≤    j
+                 --            suc (cb i) < cb (suc i) ≤ cb j
+                 --
+                 lem22 : suc (count-B i) ≡ count-B (suc i)
+                 lem22 with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+                 ... | yes _ | record { eq = eq1 } = refl
+                 ... | no nisa | _ = ⊥-elim ( nisa bi )
+                 lem23 : suc (count-B j) ≡ count-B (suc j)
+                 lem23 with is-B (fun← cn (suc j)) | inspect count-B (suc j)
+                 ... | yes _ | record { eq = eq1 } = refl
+                 ... | no nisa | _ = ⊥-elim ( nisa bj )
+                 lem24 : count-B i ≡ count-B j
+                 lem24 with  is-B (fun← cn (suc i)) | inspect count-B (suc i) | is-B (fun← cn (suc j)) | inspect count-B (suc j)
+                 ... | no nisc  | _ | _ | _ = ?
+                 ... |  yes _ | _ | no nisc | _  = ?
+                 ... |  no _ | _ | no nisc | _  = ?
+                 ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le)
+                 lem21 : suc (count-B i) ≤ count-B j
+                 lem21 = begin
+                     suc (count-B i) ≡⟨ lem22 ⟩
+                     count-B (suc i) ≤⟨ count-B-mono i<j ⟩
+                     count-B j ∎ where
+                        open ≤-Reasoning
+            lem08 : i ≡ j
+            lem08 with <-cmp i j
+            ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) )
+            ... | tri≈ ¬a b ¬c = b
+            ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq )
+
         lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB n
 
         lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
         lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0
         ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq 
-                ; cb-inject = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
-            lem12 : (cb1 : ℕ) → 1 ≡ count-B cb1 → 0 ≡ cb1
-            lem12 cb1 cbeq with <-cmp 0 cb1
-            ... | tri≈ ¬a b ¬c = b
-            ... | tri< a ¬b ¬c = ?
+                ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+            lem12 : (cb1 : ℕ) →  Is B C g (fun← cn cb1)  → 1 ≡ count-B cb1 → 0 ≡ cb1
+            lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq) 
         ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
         lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
         ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq
-                 ; cb-inject = λ cb1 cb1eq → lem12 cb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
-            lem12 : (cb1 : ℕ) → suc (count-B i)  ≡ count-B cb1 → suc i ≡ cb1
-            lem12 cb1 cbeq with <-cmp (suc i) cb1
-            ... | tri< a ¬b ¬c = ?
-            ... | tri≈ ¬a b ¬c = b
-            ... | tri> ¬a ¬b c₁ = ?
-            -- with CountB.cb-inject ( lem09 n (count-B n) ? refl  )
-            -- ... | t = ?
+                 ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+            lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → suc (count-B i)  ≡ count-B cb1 → suc i ≡ cb1
+            lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq)
         ... | no nisb | record { eq = eq1 } = lem07 n i  eq
 
         lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
@@ -812,7 +838,7 @@
            CountB.b CB  ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin
               fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩
               fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩
-              CountB.cb CB  ≡⟨ CountB.cb-inject CB _ (trans (CountB.cb=n CB) (sym eq1)) ⟩
+              CountB.cb CB  ≡⟨ CountB.cb-inject CB _ record { a = b ; fa=c = sym (fiso← cn _) }  (trans (CountB.cb=n CB) (sym eq1)) ⟩
               fun→ cn (InjectiveF.f gi b) ∎ ))  ⟩
            b  ∎  where
            open ≡-Reasoning