--- a/src/bijection.agda	Sat Jul 08 08:56:01 2023 +0900
+++ b/src/bijection.agda	Sat Aug 26 08:37:08 2023 +0900
@@ -984,34 +984,61 @@
             lem01 with cong proj2 eq
             ... | refl = refl
 
---
---  (     Bool ∷      Bool ∷ [] )    (      Bool ∷      Bool ∷ []   )  (      Bool ∷ [] )
---        true ∷      true ∷ false ∷        true ∷      true ∷ false ∷        true ∷ []
+
 
--- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln)  fi gi dec0 dec1 where
---    someday ...
-
+--  (     Bool ∷      Bool ∷ [] )  ∷ (      Bool ∷      Bool ∷ []   ) ∷     (      Bool ∷ [] )    ∷ []
+--   just true ∷ just true ∷ nothing ∷ just true ∷ just true ∷ nothing ∷      just true ∷ nothing ∷ []
+--
 LBBℕ : Bijection (List (List Bool)) ℕ
-LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ))  
-        ? ? ? ? where
+LBBℕ = Countable-Bernstein (List (Maybe Bool)) (List (List Bool)) (List (Maybe Bool)) (LMℕ Bool (bi-sym _ _ LBℕ)) (LMℕ Bool (bi-sym _ _ LBℕ))   abi bai  ? ?  where
+    atob : List (List Bool) →  List (Maybe Bool )
+    atob [] = []
+    atob ( [] ∷  t ) = nothing  ∷ atob t 
+    atob ( (h ∷ t1) ∷ t ) = just h ∷ atob (t1 ∷ t)
+ 
+    btoa : List (Maybe Bool) → List (List Bool) 
+    btoa [] = []
+    btoa (nothing ∷ t) = [] ∷ btoa t
+    btoa (just x  ∷ t) with btoa t     -- just x ∷ [] should not happen
+    ... | []    = (x ∷ []) ∷ []
+    ... | h ∷ t = (x ∷ h)  ∷ t
 
-    atob : List (List Bool) →  List Bool ∧ List Bool 
-    atob [] = ⟪ [] , [] ⟫
-    atob ( [] ∷  t ) = ⟪ false  ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫
-    atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true  ∷ proj2 ( atob t ) ⟫
+    lb00 : {A : Set } → {xa ya : A} {x y : List A} → (xa ∷ x) ≡ (ya ∷ y) → (xa ≡ ya) ∧ ( x ≡ y )
+    lb00 {A} refl = ⟪ refl , refl ⟫ 
+
+    lb01 : {A : Set } {a b : A} → just a ≡ just b → a ≡ b
+    lb01 {A} refl =  refl 
 
-    btoa : List Bool ∧ List Bool → List (List Bool) 
-    btoa ⟪ [] , _ ⟫ = []
-    btoa ⟪ _ ∷ _  , [] ⟫ = []
-    btoa ⟪ _ ∷ t0 ,  false ∷ t1  ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫ 
-    btoa ⟪ h ∷ t0 ,  true  ∷ t1  ⟫ with btoa ⟪ t0 , t1 ⟫
-    ... | [] = ( h ∷ [] ) ∷ []
-    ... | x ∷ y = (h ∷ x ) ∷ y
+    bai : InjectiveF (List (List Bool)) (List (Maybe Bool))
+    bai = record { f = atob ; inject = bai00 _ _ } where
+       bai00 : (x y : List (List Bool)) → atob x ≡ atob y → x ≡ y
+       bai00 [] [] eq = refl
+       bai00 [] ([] ∷ y₁) ()
+       bai00 [] ((x ∷ y) ∷ y₁) ()
+       bai00 ([] ∷ x₁) [] ()
+       bai00 ((x ∷ x₂) ∷ x₁) [] ()
+       bai00 ([] ∷ x₁) ([] ∷ y₁) eq = cong ([] ∷_) (bai00 _ _ (proj2 (lb00 eq)))
+       bai00 ((xa ∷ xt) ∷ xtt) ((ya ∷ yt) ∷ ytt) eq with bai00 (xt ∷ xtt) (yt ∷ ytt) (proj2 (lb00 eq))
+       ... | t = cong₂ _∷_ (cong₂ _∷_ (lb01 (proj1 (lb00 eq))) (proj1 (lb00 t))) (proj2 (lb00 t)) 
 
-Lℕ=ℕ : Bijection (List ℕ) ℕ
-Lℕ=ℕ = record {
-       fun→  = λ x → ?
-     ; fun←  = λ n → ?
-     ; fiso→ = ?
-     ; fiso← = ?
-     }
+    abi : InjectiveF (List (Maybe Bool)) (List (List Bool))
+    abi =  record { f = btoa ; inject = abi00 _ _ } where
+       abi00 : (x y : List (Maybe Bool)) → btoa x ≡ btoa y → x ≡ y
+       abi00 [] [] eq = refl
+       abi00 [] (nothing ∷ y) ()
+       abi00 [] (just x ∷ y) ()
+       abi00 (nothing ∷ x) [] ()
+       abi00 (just x ∷ x₁) [] ()
+       abi00 (just x₁ ∷ x₂) (nothing ∷ y) eq = ?
+       abi00 (nothing ∷ x₁) (just x₂ ∷ y) eq = ?
+       abi00 (nothing ∷ x) (nothing ∷ y) eq = cong (nothing ∷_) (abi00 _ _ (proj2 (lb00 eq)))
+       abi00 (just x ∷ x₁) (just y ∷ y₁) eq with btoa x₁ | btoa y₁ | inspect btoa x₁ | inspect btoa y₁
+       ... | [] | [] | record { eq = eq1 } | record { eq = eq2 } = cong₂ _∷_ (cong just abi01) (abi00 _ _ (trans eq1 (sym eq2))) where
+           abi01 : x ≡ y 
+           abi01 = proj1 (lb00 (proj1 (lb00 eq)))
+       ... | [] | t ∷ t₁ | record { eq = eq1}  | record { eq = eq2}  = ?
+       ... | s ∷ s₁ | [] | _ | _ = ?
+       ... | s ∷ s₁ | t ∷ t₁ | record { eq = eq1}  | record { eq = eq2}  = ?
+
+
+-- Lℕ=ℕ : Bijection (List ℕ) ℕ