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

diff -r 7ef12a53bfb0 -r d1b6fb58aad0 src/bijection.agda
--- a/src/bijection.agda	Sat Aug 26 10:28:54 2023 +0900
+++ b/src/bijection.agda	Sat Aug 26 10:36:09 2023 +0900
@@ -984,97 +984,21 @@
             lem01 with cong proj2 eq
             ... | 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 = ?
-
+-- we may need substraction
+--
+-- bi-subtract : (A B : Set ) → Bijection (A ∨ B) ℕ → finiteSet B → Bijection A ℕ
+--
+-- Maybeℕ : (A : Set ) → Bijection (Maybe A) ℕ → Bijection A ℕ
+--
 --  (     Bool ∷      Bool ∷ [] )  ∷ (      Bool ∷      Bool ∷ []   ) ∷     (      Bool ∷ [] )    ∷ []
 --   just true ∷ just true ∷ nothing ∷ just true ∷ just true ∷ nothing ∷      just true ∷ nothing ∷ []
 --
-LBBℕ : Bijection (List (List Bool)) ℕ
-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) → Maybe (List (List Bool) )
-    btoa [] = just []
-    btoa (nothing ∷ t) = just ([] ∷ btoa t)
-    btoa (just x  ∷ t) with btoa t     -- just x ∷ [] should not happen
-    ... | 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 ⟫ 
-
-    lb01 : {A : Set } {a b : A} → just a ≡ just b → a ≡ b
-    lb01 {A} refl =  refl 
-
-    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)) 
-
-    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}  = ?
+-- LBBℕ : Bijection (List (List Bool)) ℕ
+--          
+-- Lℕ=ℕ : Bijection (List ℕ) ℕ
+--
 
 
--- Lℕ=ℕ : Bijection (List ℕ) ℕ
+
+
+