# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686098578 -32400
# Node ID 66a6804d867b44df7d6114e669cdc4ff57eae00f
# Parent  c97660e1953562ad7d47610b4a794919688839ba
...

diff -r c97660e19535 -r 66a6804d867b src/OD.agda
--- a/src/OD.agda	Mon Jun 05 14:50:02 2023 +0900
+++ b/src/OD.agda	Wed Jun 07 09:42:58 2023 +0900
@@ -343,6 +343,10 @@
 union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
 union← X z UX∋z not = ⊥-elim ( not (* (Own.owner UX∋z)) ⟪ subst (λ k → odef X k) (sym &iso) ( Own.ao UX∋z) , Own.ox UX∋z ⟫  )
 
+--
+--
+--
+
 record RCod (COD : HOD) (ψ : HOD → HOD)  : Set (suc n) where
  field
      ≤COD : ∀ {x : HOD } → ψ x ⊆ COD 
diff -r c97660e19535 -r 66a6804d867b src/ZProduct.agda
--- a/src/ZProduct.agda	Mon Jun 05 14:50:02 2023 +0900
+++ b/src/ZProduct.agda	Wed Jun 07 09:42:58 2023 +0900
@@ -362,7 +362,7 @@
    field
        i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
        iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x lt )
-       iiso : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y
+       inject : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y
 
 record HODBijection (A B : HOD ) : Set n where
    field
diff -r c97660e19535 -r 66a6804d867b src/bijection.agda
--- a/src/bijection.agda	Mon Jun 05 14:50:02 2023 +0900
+++ b/src/bijection.agda	Wed Jun 07 09:42:58 2023 +0900
@@ -475,8 +475,96 @@
         lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x
         lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1)) 
 
-Bernstein : (A B C D : Set) → Bijection A D → Bijection C D → (f : A → B ) → (g : B → C )  → Bijection B D
-Bernstein A B C D ad cd f g = ?
+-- Bernstein is non constructive, so we cannot use this without some assumption
+--   but in case of ℕ, we can construct it directly.
+
+record InjectiveF (A B : Set) : Set where
+   field
+      f : A → B
+      inject : {x y : A} → f x ≡ f y → x ≡ y
+
+record Is (A C : Set) (f : A → C) (c : C) : Set where
+   field
+      a : A
+      fa=c : f a ≡ c
+
+Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ 
+     → (fi : InjectiveF A  B ) → (gi : InjectiveF  B C )  
+     → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c)  )
+     → Bijection B ℕ
+Countable-Bernstein A B C an cn fi gi is-A is-B = record {
+       fun→  = λ x → bton x
+     ; fun←  = λ n → ntob n
+     ; fiso→ = λ n → ?
+     ; fiso← = λ x → ?
+   } where
+    --
+    --     an     f     g     cn
+    --   ℕ →   A  →  B  →  C  →   ℕ
+    --
+    open Bijection
+    f = InjectiveF.f fi
+    g = InjectiveF.f gi
+
+    cbn : ℕ → ℕ
+    cbn n = fun→ cn (g (f (fun← an (suc n))))
+
+    --
+    -- count number of valid A and B in C
+    --     the count of B is the numner of B in Bijection B ℕ
+    --     if we have a , number a of A is larger than the numner of B C, so we have the inverse
+    --
+    record CB (n : ℕ) : Set where
+      field
+         ca cb : ℕ
+         cb≤n  : cb ≤ suc n  
+         ca≤cb : ca ≤ cb  
+         na : {i : ℕ} → i < ca → A
+         nb : {i : ℕ} → i < cb → B
+         ia : {i j : ℕ } → { i<c : i < ca } → {j<c : j < ca } → na i<c ≡ na j<c → i ≡ j
+         ib : {i j : ℕ } → { i<c : i < cb } → {j<c : j < cb } → nb i<c ≡ nb j<c → i ≡ j
+
+    ¬isA∧isB : (y : C ) →  Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥
+    ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where
+         lem : g (f (Is.a isa)) ≡ y
+         lem = begin
+           g (f (Is.a isa))  ≡⟨ Is.fa=c isa  ⟩
+           y ∎ where
+             open ≡-Reasoning
+
+    lb : (n : ℕ ) → CB n
+    lb zero with is-A (fun← cn zero) | is-B (fun← cn zero)
+    ... | yes isA | yes isB =  record { ca = suc zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ≤-refl ; na = λ _ → Is.a isA ; nb = λ _ → Is.a isB ; ia = ? ; ib = ? } 
+    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB = record { ca = zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ? ; na = λ () ; nb = ? ; ia = ? ; ib = ? } 
+    ... | no nisA | no nisB = record { ca = zero ; cb = zero ; cb≤n = ? ; ca≤cb = ? ; na = λ () ; nb = λ () ; ia = ? ; ib = ? } 
+    lb (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n))
+    ... | yes isA | yes isB =  record { ca = suc (CB.ca (lb n)) ; cb = suc (CB.cb (lb n)) ; cb≤n = ? ; ca≤cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } 
+    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB = record { ca = CB.ca (lb n) ; cb = suc (CB.cb (lb n)) ; cb≤n = ? ; ca≤cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } 
+    ... | no nisA | no nisB = record { ca = CB.ca (lb n) ; cb = CB.cb (lb n) ; cb≤n = ? ; ca≤cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } 
+    -- record { ca = ? ; cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } where
+    --    cbn : CB n
+    --    cbn = lb n
+    -- 
+
+    cb< : (n : ℕ) → CB.cb (lb (cbn n)) < CB.cb (lb (cbn (suc n)))
+    cb< = ?
+          
+    n<cbn : (n : ℕ) →  n < CB.cb (lb (cbn n))
+    n<cbn zero = ?
+    n<cbn (suc n) = begin
+       suc (suc n)  ≤⟨ s≤s (n<cbn n) ⟩  
+       suc (CB.cb (lb (cbn n)))  ≤⟨ cb< n ⟩
+       CB.cb (lb (cbn (suc n)))  ∎  where
+          open ≤-Reasoning
+
+    bton : B → ℕ
+    bton b = CB.cb (lb (fun→ cn (g b)))
+    ntob : ℕ → B
+    ntob n = CB.nb (lb (fun→ cn (g (f (fun← an (suc n)))))) {n} (n<cbn n)
+
+
 
 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 {
@@ -495,36 +583,49 @@
 LM1 : (A : Set ) → Bijection (List A ) ℕ → Bijection (List A ∧ List Bool) ℕ
 LM1 A Ln = bi-trans (List A ∧ List Bool) (ℕ ∧ ℕ)  ℕ (bi-∧ Ln (bi-sym _ _ LBℕ) ) (bi-sym _ _ nxn)
 
+open import Data.List.Properties
+open import Data.Maybe.Properties
+
 LMℕ : (A : Set ) → Bijection (List A) ℕ → Bijection (List (Maybe A)) ℕ
-LMℕ A Ln = Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) ℕ Ln (LM1 A Ln)  f g where
+LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln)  fi gi ? ? where
    f : List A → List (Maybe A)
    f [] = []
-   f (x ∷ t) = just x ∷ f t
+   f (x ∷ t) = just x ∷ f t 
+   f-inject : {x y : List A} → f x ≡ f y → x ≡ y
+   f-inject {[]} {[]} refl = refl
+   f-inject {x ∷ xt} {y ∷ yt} eq = cong₂ (λ j k → j ∷ k ) (just-injective (∷-injectiveˡ eq)) (f-inject (∷-injectiveʳ eq) )
    g : List (Maybe A) → List A ∧ List Bool
    g [] = ⟪ [] , [] ⟫
    g (just h ∷ t)  = ⟪ h ∷ proj1 (g t) , true  ∷ proj2 (g t) ⟫
    g (nothing ∷ t) = ⟪     proj1 (g t) , false ∷ proj2 (g t) ⟫
+   g⁻¹ :  List A ∧ List Bool → List (Maybe A) 
+   g⁻¹ ⟪ [] , [] ⟫ = []
+   g⁻¹ ⟪ x ∷ xt , [] ⟫ = just x ∷  g⁻¹ ⟪ xt , [] ⟫ 
+   g⁻¹ ⟪ [] , true ∷ y ⟫ = []
+   g⁻¹ ⟪ x ∷ xt , true ∷ yt ⟫ = just x ∷ g⁻¹ ⟪ xt , yt ⟫
+   g⁻¹ ⟪ [] , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ [] , y ⟫  
+   g⁻¹ ⟪ x ∷ x₁ , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ x ∷ x₁ , y ⟫
+   g-iso : {x : List (Maybe A)} → g⁻¹ (g x) ≡ x
+   g-iso {[]} = refl
+   g-iso {just x ∷ xt} = cong ( λ k → just x ∷ k) ( g-iso )
+   g-iso {nothing ∷ []} = refl
+   g-iso {nothing ∷ just x ∷ xt} = cong (λ k → nothing ∷ k ) ( g-iso {_} )
+   g-iso {nothing ∷ nothing ∷ xt} with g-iso {nothing ∷ xt} 
+   ... | t = trans (lemma01 (proj1 (g xt)) (proj2 (g xt)) ) ( cong (λ k → nothing ∷ k ) t ) where 
+         lemma01 : (x : List A) (y : List Bool ) →  g⁻¹ ⟪ x , false ∷ false ∷ y ⟫ ≡ nothing ∷ g⁻¹ ⟪ x , false ∷ y ⟫
+         lemma01 [] y = refl
+         lemma01 (x ∷ x₁) y = refl
+   g-inject : {x y : List (Maybe A)} → g x ≡ g y → x ≡ y
+   g-inject {x} {y} eq = subst₂ (λ j k → j ≡ k ) g-iso g-iso (cong g⁻¹ eq )
+   fi : InjectiveF (List A) (List (Maybe A))
+   fi = record { f = f ; inject = f-inject  }
+   gi : InjectiveF (List (Maybe A)) (List A ∧ List Bool )
+   gi = record { f = g ; inject = g-inject }
 
 -- open import Data.Fin
 --
---- record LF (n m : ℕ) (lton : List (Fin n) → ℕ ) : Set where
----   field
----      nlist : List Bool
----      isBin : lton nlist ≡ m
----      isUnique :  (x : List Bool) → lton x ≡ m → nlist  ≡ x 
---- 
---- lb+1 : {n : ℕ) → List Bool → List Bool
---- lb+1 [] =  false ∷ [] 
---- lb+1 (false ∷ t) = true ∷ t 
---- lb+1 (true ∷ t) =  false ∷ lb+1 t
---- 
---- lb-1 : {n : ℕ) → List Bool → List Bool
---- lb-1 [] =  []
---- lb-1 (true ∷ t) = false ∷ t 
---- lb-1 (false ∷ t) with lb-1 t
---- ... | [] = true ∷ []
---- ... | x ∷ t1 = true ∷ x ∷ t1
-
+--- LBFin : {n : ℕ } → Bijection (List (Meybe (Fin n))) ( List (Fin (suc n))) 
+--
 --- LBFin : {n : ℕ } → Bijection ℕ ( List (Fin n)) 
 --- LBFin = ?
 
diff -r c97660e19535 -r 66a6804d867b src/cardinal.agda
--- a/src/cardinal.agda	Mon Jun 05 14:50:02 2023 +0900
+++ b/src/cardinal.agda	Wed Jun 07 09:42:58 2023 +0900
@@ -102,7 +102,7 @@
         be01 : i→ iab x ax ≡ x
         be01 = ?
         be02 : x ≡  i→ iba x ?
-        be02 = iiso iab ? ? ax ( iB iba _ ? ) ? 
+        be02 = inject iab ? ? ax ( iB iba _ ? ) ? 
     b⊆a : * b ⊆ * a
     b⊆a bx = ?
     be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥