# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1693013334 -32400
# Node ID 7ef12a53bfb0b034e3a42cd990a322453ef0588a
# Parent  171c3f3cdc6b491254076a94b48eebc3eea093d7
...

diff -r 171c3f3cdc6b -r 7ef12a53bfb0 src/bijection.agda
--- a/src/bijection.agda	Sat Aug 26 08:37:08 2023 +0900
+++ b/src/bijection.agda	Sat Aug 26 10:28:54 2023 +0900
@@ -985,23 +985,59 @@
             ... | refl = refl
 
 
+Maybeℕ : (A : Set ) → Bijection (Maybe A) ℕ → Bijection A ℕ
+Maybeℕ A ba with fun→ ba nothing | inspect (fun→ ba) nothing 
+... | zero | record { eq = eq1 } = record {
+       fun←  = ?
+     ; fun→  = ?
+     ; fiso← = ?
+     ; fiso→ = ?
+  } where
+    f00 : ℕ → A
+    f00 x with fun← ba (suc x)
+    ... | nothing = ?
+    ... | just a = a
+... | suc nz | record { eq = eq1 } =  record {
+       fun←  = ?
+     ; fun→  = ?
+     ; fiso← = ?
+     ; fiso→ = ?
+  } where
+    -- if we have two nothing in the range of fun← ba, fiso← will fail.
+    f02 : (x : ℕ ) → ¬ (fun← ba x ≡ nothing )  → A
+    f02 = ?
+    f00 : ℕ → A
+    f00 x with <-cmp (fun→ ba nothing) x
+    ... | tri< a ¬b ¬c = ?
+    ... | tri≈ ¬a b ¬c = ?
+    ... | tri> ¬a ¬b c = ?
+    f01 : A → ℕ
+    f01 x with <-cmp (fun→ ba nothing) (fun→ ba (just x))
+    ... | tri< a ¬b ¬c = ?
+    ... | tri≈ ¬a b ¬c = ?
+    ... | tri> ¬a ¬b c = ?
 
 --  (     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 (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 [] = []
+LBBℕ = Maybeℕ _ lb02 where
+    lb02 : Bijection (Maybe (List (List Bool))) ℕ
+    lb02 = Countable-Bernstein (List (Maybe Bool)) (Maybe (List (List Bool))) (List (Maybe Bool)) 
+        (LMℕ Bool (bi-sym _ _ LBℕ)) (LMℕ Bool (bi-sym _ _ LBℕ))   ? ? ? ?  
+    atob : Maybe (List (List Bool)) →  List (Maybe Bool )
+    atob nothing = []
+    atob just [] = []
     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 : List (Maybe Bool) → Maybe (List (List Bool) )
+    btoa [] = just []
+    btoa (nothing ∷ t) = just ([] ∷ btoa t)
     btoa (just x  ∷ t) with btoa t     -- just x ∷ [] should not happen
-    ... | []    = (x ∷ []) ∷ []
-    ... | h ∷ t = (x ∷ h)  ∷ t
+    ... | just []    = just ((x ∷ []) ∷ [])
+    ... | just (h ∷ [] ) = nothing
+    ... | just (h ∷ h1 ∷ t ) = just ( (x ∷ h ∷ h1)  ∷ t )
 
     lb00 : {A : Set } → {xa ya : A} {x y : List A} → (xa ∷ x) ≡ (ya ∷ y) → (xa ≡ ya) ∧ ( x ≡ y )
     lb00 {A} refl = ⟪ refl , refl ⟫