# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687492037 -32400
# Node ID 082d83168e25d4ada751102e4fd226f02ac73025
# Parent  9ef69be89d06a71233c533638558380d93006e4f
...

diff -r 9ef69be89d06 -r 082d83168e25 src/bijection.agda
--- a/src/bijection.agda	Fri Jun 23 11:49:24 2023 +0900
+++ b/src/bijection.agda	Fri Jun 23 12:47:17 2023 +0900
@@ -726,24 +726,25 @@
           cb : ℕ
           b=cn : fun← cn cb ≡ g b
           cb=n : count-B cb ≡ suc n
-          cb-inject : (b1 : B) → count-B (fun→ cn (g b)) ≡ count-B (fun→ cn (g b1)) → b ≡ b1
+          cb-inject : (cb1 : ℕ) → count-B cb ≡ count-B cb1 → cb ≡ cb1
 
     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
+        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 = lem12 } where
+        ... | 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 = ? } where
             lem12 : (b2 : B) → count-B (fun→ cn (g (Is.a isb))) ≡ count-B (fun→ cn (g b2)) → Is.a isb ≡ b2
             lem12 b2 eq = ?
         ... | 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 = lem12 } where
+        ... | 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 = ? } where
             lem12 : (b2 : B) → count-B (fun→ cn (g (Is.a isb))) ≡ count-B (fun→ cn (g b2)) → Is.a isb ≡ b2
             lem12 b2 eq = ?
         ... | no nisb | record { eq = eq1 } = lem07 n i  eq
 
-        lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB n
         lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
         ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
         ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0
@@ -793,7 +794,19 @@
            open ≡-Reasoning
            CB  = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
            lem26 : count-B (fun→ cn (g (CountB.b CB))) ≡ count-B (fun→ cn (g b))  → CountB.b CB ≡ b
-           lem26 = CountB.cb-inject CB _
+           lem26 eq = begin
+               CountB.b CB ≡⟨ InjectiveF.inject gi ( begin 
+                  g (CountB.b CB) ≡⟨ 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 _ ( begin
+                         count-B (CountB.cb CB)  ≡⟨ cong count-B ? ⟩
+                         count-B (fun→ cn (g (CountB.b CB)))  ≡⟨ eq ⟩
+                         count-B (fun→ cn (g b)) ∎ ) ⟩
+                      fun→ cn (g b) ∎ ) ⟩
+                  g b ∎ ) ⟩
+               b ∎ 
+               --  ? ≡⟨ cong (fun← cn) (CountB.cb-inject CB _ ?) ⟩
 
 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 {