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

diff -r 79cf38cc667b -r 171c3f3cdc6b Todo
--- a/Todo	Sat Jul 08 08:56:01 2023 +0900
+++ b/Todo	Sat Aug 26 08:37:08 2023 +0900
@@ -1,3 +1,8 @@
+Sun Jul  9 09:42:20 JST 2023
+
+    Assume countable dense OD in Ordinal as L
+    if Power ω ∩ L is cardinal, ω c< (Power ω ∩ L) c< Power ω 
+
 Sat May 13 10:51:35 JST 2023
 
     use Filter (ZFP (Proj1 (ZFP PQ)) (Proj2 (ZFP PQ)) for projection of Ultra filter
@@ -6,12 +11,15 @@
 Sat Aug  1 13:16:53 JST 2020
 
     P Generic Filter
-        as a ZF model 
-    define Definition for L
+        as a ZF model   ( -- this is no good )
+    define Definition for L  ( -- this is no good )
 
 Tue Jul 23 11:02:50 JST 2019
 
     define cardinals     ... done
+
+    scheme on CH is no good in HOD
+
     prove CH in OD→ZF
     define Ultra filter  ... done
     define L M : ZF ZFSet = M is an OD
diff -r 79cf38cc667b -r 171c3f3cdc6b src/VL.agda
--- a/src/VL.agda	Sat Jul 08 08:56:01 2023 +0900
+++ b/src/VL.agda	Sat Aug 26 08:37:08 2023 +0900
@@ -36,50 +36,38 @@
 --    V α + 1 := P ( V α ) 
 --    V α := ⋃ { V β | β < α }
 
-V : ( β : Ordinal ) → HOD
-V β = TransFinite  V1 β where
-   V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
-   V1 x V0 with trio< x o∅
-   V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
-   V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅
-   V1 x V0 | tri> ¬a ¬b c with Oprev-p  x
-   V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
-   V1 x V0 | tri> ¬a ¬b c | no ¬p = 
-        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (V0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
+V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
+V1 x V0 with trio< x o∅
+V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
+V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅
+V1 x V0 | tri> ¬a ¬b c with Oprev-p  x
+V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
+V1 x V0 | tri> ¬a ¬b c | no ¬p = 
+    record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (V0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
 
---
--- L ⊆ HOD ⊆ V
---
--- HOD=V : (x : HOD) → V (odmax x) ∋ x
--- HOD=V x = {!!}
+record VOrd (x : Ordinal) : Set n where
+   field 
+     β : Ordinal
+     ov : odef (TransFinite  V1 β) x 
 
---
--- Definition for Power Set
---
-record Definitions  : Set (suc n) where 
-   field
-      Definition : HOD → HOD   
+V : OD
+V = record { def = λ x → VOrd x }
 
-open Definitions
-
-Df : Definitions → (x : HOD) → HOD
-Df D x = Power x ∩ Definition D x 
+record Vn : Set n where
+   field
+     x  : Ordinal
+     β  : Ordinal
+     ov : odef (TransFinite  V1 β) x 
 
--- The constructible Sets
---    L 0 := ∅ 
---    L α + 1 := Df (L α)   -- Definable Power Set
---    V α := ⋃ { L β | β < α }
+Vn∅ : Vn
+Vn∅ = record { x = o∅ ; β = o∅ ; ov = ? }
 
-L : ( β : Ordinal ) → Definitions → HOD
-L β D = TransFinite  L1 β where
-   L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
-   L1 x L0 with trio< x o∅
-   L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
-   L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅
-   L1 x L0 | tri> ¬a ¬b c with Oprev-p  x
-   L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
-   L1 x L0 | tri> ¬a ¬b c | no ¬p = 
-        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (L0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
+vsuc : Vn → Vn
+vsuc v = ?
 
-V=L0 : Set (suc n)
-V=L0 = (x : Ordinal) → V x ≡  L x record { Definition = λ y → y }
+v< : Vn → Vn → Set n
+v< x y = ?
+
+IsVOrd : IsOrdinals Vn Vn∅ vsuc ?
+IsVOrd = ?
+
diff -r 79cf38cc667b -r 171c3f3cdc6b src/bijection.agda
--- 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 ℕ) ℕ
diff -r 79cf38cc667b -r 171c3f3cdc6b src/cardinal.agda
--- a/src/cardinal.agda	Sat Jul 08 08:56:01 2023 +0900
+++ b/src/cardinal.agda	Sat Aug 26 08:37:08 2023 +0900
@@ -145,8 +145,24 @@
       gf = record { i→ = λ x ax → g (f x ax) (b∋f x ax) ; iB = λ x ax → a∋g _ (b∋f x ax) 
          ; inject = λ x y ax ay eq → f-inject _ _ ax ay ( g-inject _ _ (b∋f _ ax) (b∋f _ ay) eq) } 
 
+      -- HOD UC is closure of gi ∙ fi starting from a - Image g
+      -- and a-UC is the remaining part of a. Both sets have inverse functions.
       --
-      -- HOD UC is closure of gi ∙ fi starting from a - Image g
+      -- We cannot directly create h : * a → * b from these functions, because
+      -- the choise of UC ∨  a-UC is non constructive and
+      -- LEM cannot be used in this non positive context. 
+      --
+      -- We use the following trick:
+      --
+      --    bi-UC  : HODBijection UC fUC
+      --    bi-fUC : HODBijection a-UC b-fUC
+      --
+      -- The HODBijection (* a) (* b) is a merge of these bijections.
+      -- The merging bi-UC and  bi-fUC uses also LEM but use it positively.
+      --
+      -- bijection on each side is easy, because these are images of fi and g.
+      --    somehow we don't use injection of f.
+      --
       --
       data gfImage :  (x : Ordinal) → Set n where
           a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a gi x )) → gfImage  x
@@ -258,12 +274,6 @@
       fU-iso0 {x} (a-g ax ¬ib) = refl 
       fU-iso0 {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt) = refl
 
-      --
-      -- We cannot directly create h : * a → * b , because the cnoise of UC ∨  a-UC is non constructive and
-      -- even LEM cannot be used in positive context. The merging bi-UC and  bi-fUC uses also LEM but use it positively.
-      --
-      -- bijection on each side is easy, because these are images of fi and g.
-      --    somehow we don't use injection of f.
 
       bi-UC : HODBijection UC fUC
       bi-UC = record { 
@@ -303,9 +313,6 @@
 _c<_ : ( A B : HOD ) → Set n
 A c< B = ¬ ( Injection (& B)  (& A) )
 
-Card : OD
-Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ HODBijection (* a) (* x) }
-
 record Cardinal (a : Ordinal ) : Set (Level.suc n) where
    field
        card : Ordinal
@@ -316,10 +323,7 @@
 -- Cardinal∈ = {!!}
 
 -- Cardinal⊆ : { s t : HOD } → s ⊆ t →  ( s c< t ) ∨ ( s =c= t ) -- this is not valid
--- Cardinal⊆ = {!!}
-
--- HBool : HOD
--- HBool = record { od = record { def = λ x → (x ≡ o∅) ∨ (x ≡ osuc o∅ ) } ; odmax = osuc (osuc o∅) ; <odmax = ? }
+-- Cardinal⊆ = {!!}                                              -- we may have infinite sets with the same cardinality
 
 PtoF : {u : HOD} {x s : Ordinal } → odef (Power u) s → odef u x → Bool
 PtoF {u} {x} {s} su ux with ODC.p∨¬p O (odef (* s) x )
@@ -356,7 +360,7 @@
              c01 y (case2 eq) = subst₂ (λ j k  → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt
      f2 : Injection (& (Power S)) (& S) 
      f2 = f
-     postulate 
+     postulate   -- yes we have a proof but it is very slow
          b : HODBijection (Power S) S 
      -- b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)   -- this makes check very slow
      --      but postulate makes check weak eg. irrerevance of ∋ 
diff -r 79cf38cc667b -r 171c3f3cdc6b src/generic-filter.agda
--- a/src/generic-filter.agda	Sat Jul 08 08:56:01 2023 +0900
+++ b/src/generic-filter.agda	Sat Aug 26 08:37:08 2023 +0900
@@ -51,6 +51,19 @@
 
 open import ZProduct O
 
+-- L   :   definable HOD in Agda
+--    L  Countable
+--    Dense in Ordinal
+
+---  Dense   L
+--      x : Ord → ∃ l ∈ L → x ⊆ l
+--
+--     ω  =c=  Power ω　∩ L        c< Power ω
+--     ω  c<   Power ω　∩ G[L]     c< Power ω    -- CH counter example
+--                 Power (G[L]) 
+--
+
+
 record CountableModel : Set (Level.suc (Level.suc n)) where
    field
        ctl-M : HOD
@@ -69,27 +82,6 @@
 
 -- we expect  P ∈ * ctl-M ∧ G  ⊆ L ⊆ Power P  , ¬ G ∈ * ctl-M,
 
-record COD : Set (Level.suc (Level.suc n)) where
-   field
-       CO : Ordinals {n}
-       CA : OD.ODAxiom CO
-       cod→ : ℕ → Ordinals.Ordinal CO
-       cod← : Ordinals.Ordinal CO → ℕ
-       cod-iso→ : { x : Ordinals.Ordinal CO } → cod→ (cod← x) ≡ x
-       cod-iso← : { x : ℕ } → cod← (cod→ x) ≡ x
-       -- Since it is countable, it is HOD.
-
--- CM : COD → CountableModel 
--- CM cod = record { 
---       ctl-M = ?
---     ; ctl→ = λ n → ?
---     ; ctl<M = λ n → ?
---     ; ctl← = λ x → ?
---     ; ctl-iso→ = ?
---     ; TC = ?
---     ; is-model = ?
---       }
-
 open CountableModel
 
 ----
@@ -392,52 +384,4 @@
 --     M ⊆ M[G]
 --     M[G] ∋ G
 --     M[G] ∋ ∪G
---
---     assume countable L as M
---     L is a countable subset of Power ω i.e. Power ω ∩ M
---     it defines countable Ordinal
---
---  Generic Filter is a countable sequence of element of M
---    Mg is set of all elementns of M which contains an element of G
---
---  Mg : HOD
---  Mg 
 
-record Mg {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) (x : Ordinal) : Set n where
-    field
-       gi : Ordinal
-       G∋gi : odef (⊆-Ideal.ideal (genf G)) gi
-       x∋gi : odef (* x) gi
-
-MgH : {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) → HOD
-MgH {L} {P} LP M G = record { od = record { def = λ x → (x o< & M) ∧ Mg LP M G x } ; odmax = & M ; <odmax = proj1  }
-
-MG1 : {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) → HOD
-MG1 {L} {P} LP M G = M ∪ Union (MgH LP M G)
-
-TCS : (G : HOD) → Set (Level.suc n)
-TCS G = {x y : HOD} → G ∋ x → x ∋ y → G ∋ y
-
-GH : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
-      → (C : CountableModel ) → HOD
-GH P L p0 LPP Lp0 C = ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))
--- 
--- module _ {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (GF : GenericFilter {L} {P} LP M) where
--- 
---     MG = MG1 {L} {P} LP M GF 
---     G = ⊆-Ideal.ideal (genf GF)
--- 
---     M⊆MG : M ⊆ MG 
---     M⊆MG = case1
--- 
---     MG∋G : MG ∋ G
---     MG∋G = case2 record { owner = ? ; ao = ? ; ox = ? } where
---        gf00 : ?
---        gf00 = ?
--- 
---     MG∋UG : MG ∋ Union G
---     MG∋UG = case2 record { owner = ? ; ao = ? ; ox = ? } where
---        gf00 : ?
---        gf00 = ?
--- 
---