# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1647247876 -32400
# Node ID b27d92694ed53bfd6ef44f06cb06650f3c8084ac
# Parent  be685f338fdc00c3c9cf5e5d3e3072389831e5db
...

diff -r be685f338fdc -r b27d92694ed5 src/BAlgbra.agda
--- a/src/BAlgbra.agda	Sun Mar 13 19:22:12 2022 +0900
+++ b/src/BAlgbra.agda	Mon Mar 14 17:51:16 2022 +0900
@@ -37,6 +37,9 @@
 --A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
 --    odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }
 
+∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A)
+∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ =  λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ }
+
 _∪_ : ( A B : HOD  ) → HOD
 A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
     odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
diff -r be685f338fdc -r b27d92694ed5 src/OD.agda
--- a/src/OD.agda	Sun Mar 13 19:22:12 2022 +0900
+++ b/src/OD.agda	Mon Mar 14 17:51:16 2022 +0900
@@ -216,7 +216,7 @@
 ∅< : { x y : HOD  } → odef x (& y ) → ¬ (  od x  == od od∅  )
 ∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
 ∅<  {x} {y} d eq | lift ()
-       
+
 ∅6 : { x : HOD  }  → ¬ ( x ∋ x )    --  no Russel paradox
 ∅6  {x} x∋x = o<¬≡ refl ( c<→o<  {x} {x} x∋x )
 
diff -r be685f338fdc -r b27d92694ed5 src/filter.agda
--- a/src/filter.agda	Sun Mar 13 19:22:12 2022 +0900
+++ b/src/filter.agda	Mon Mar 14 17:51:16 2022 +0900
@@ -124,9 +124,9 @@
    field
        dense : HOD
        d⊆P :  dense ⊆ Power P 
-       dense-f : HOD → HOD
-       dense-d :  { p : HOD} → p ⊆ P → dense ∋ dense-f p  
-       dense-p :  { p : HOD} → p ⊆ P → p ⊆ (dense-f p) 
+       dense-f : {p : HOD} → p ⊆ P → HOD
+       dense-d :  { p : HOD} → (lt : p ⊆ P) → dense ∋ dense-f lt
+       dense-p :  { p : HOD} → (lt : p ⊆ P) → p ⊆ (dense-f lt) 
 
 record Ideal  ( L : HOD  ) : Set (suc n) where
    field
@@ -168,15 +168,15 @@
    field
        dense : L → Set n
        d⊆P :  PL dense 
-       dense-f : L → L 
-       dense-d :  { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p  )
-       dense-p :  { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) 
+       dense-f : {p : L}  → PL (λ x → p ⊆ x ) → L 
+       dense-d :  { p : L} → (lt : PL (λ x → p ⊆ x )) → dense ( dense-f lt  )
+       dense-p :  { p : L} → (lt : PL (λ x → p ⊆ x )) → p ⊆ (dense-f lt) 
 
 Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
 Dense-is-F {L} f = record {
        dense =  λ x → Lift (suc n) ((dense f) ∋ x)
     ;  d⊆P = λ x f∋x →  power→⊆ _ _ (incl ( d⊆P f  ) (lower f∋x ))
-    ;  dense-f = λ x → dense-f f x
+    ;  dense-f = λ {p} lt → dense-f f (lt _ record { incl = λ x → x} ) 
     ;  dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) )
     ;  dense-p = λ {p} d → dense-p f (d p refl-⊆) 
   } where open Dense
diff -r be685f338fdc -r b27d92694ed5 src/generic-filter.agda
--- a/src/generic-filter.agda	Sun Mar 13 19:22:12 2022 +0900
+++ b/src/generic-filter.agda	Mon Mar 14 17:51:16 2022 +0900
@@ -68,7 +68,6 @@
 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
 -- 
 
-
 -- we expect  P ∈ * ctl-M ∧ G  ⊆ Power P  , ¬ G ∈ * ctl-M, 
 
 open CountableModel 
@@ -92,7 +91,7 @@
 ... | no not  = & (ODC.minimal O ( PGHOD i P C (find-p P C i x)) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
 
 ---
--- G = { r ∈ Power P | ∃ n → p(n) ⊆ q }
+-- G = { r ∈ Power P | ∃ n → p(n) ⊆ r }
 --
 record PDN  (P p : HOD ) (C : CountableModel P)  (x : Ordinal) : Set n where
    field
@@ -168,7 +167,6 @@
                f5 : odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (find-p P C (gr PD∋q) (& p0))) y
                f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋p} {gr PD∋q} (<to≤ a))
                    (subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) (sym &iso) lt) )
---    subst (λ k → odef k y) *iso (pn<gr PD∋q y (subst (λ k → odef _ k ) &iso (incl (p-monotonic _ _ C a ) (subst (λ k → odef _ k) &iso lt) ))) ⟫
         ... | tri≈ ¬a refl ¬c = record { gr = gr PD∋p ;  pn<gr =  λ y lt → subst (λ k → odef k y ) (sym *iso) (f4 y lt);  x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
             f4 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
             f4 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ 
@@ -181,39 +179,68 @@
         fdense : (D : Dense P ) → ¬ (filter.Dense.dense D ∩ PDHOD P p0 C) ≡ od∅
         fdense D eq0  = ⊥-elim (  ∅< {Dense.dense D ∩ PDHOD P p0 C} fd01 (≡od∅→=od∅ eq0 )) where
            open Dense
+           p0⊆P : p0 ⊆ P
+           p0⊆P = ODC.power→⊆ O _ _ Pp0
            fd : HOD
-           fd = dense-f D p0
+           fd = dense-f D p0⊆P
            PP∋D : dense D ⊆ Power P
            PP∋D = d⊆P D
            fd00 : PDHOD P p0 C ∋ p0
            fd00 = record { gr = 0 ; pn<gr = λ y lt → lt ; x∈PP = Pp0 }
-           fd02 : dense D ∋ dense-f D p0 
-           fd02 = dense-d D (ODC.power→⊆ O _ _ Pp0 )
-           fd04 : dense-f D p0 ⊆ P
+           fd02 : dense D ∋ dense-f D p0⊆P
+           fd02 = dense-d D p0⊆P
+           fd04 : dense-f D p0⊆P ⊆ P
            fd04 = ODC.power→⊆ O _ _ ( incl PP∋D fd02 )
-           fd03 : PDHOD P p0 C  ∋ dense-f D p0 
-           fd03 = f1 {p0} {dense-f D p0} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) )
+           fd03 : PDHOD P p0 C  ∋ dense-f D p0⊆P
+           fd03 = f1 {p0} {dense-f D p0⊆P} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) )
            fd01 : (dense D ∩ PDHOD P p0 C) ∋ fd
            fd01 = ⟪ fd02 , fd03 ⟫ 
 
-
-
-
 open GenericFilter
 open Filter
 
-record Incompatible  (P : HOD ) : Set (suc (suc n)) where
+record Incompatible  (P p : HOD ) (PP∋p : p  ⊆ P ) : Set (suc (suc n)) where
    field
-      q : {p : HOD } → Power P ∋ p → HOD 
-      r : {p : HOD } → Power P ∋ p → HOD 
-      incompatible : { p : HOD } →  (P∋p : Power P ∋ p)  →  Power P ∋ q P∋p  →  Power P ∋ r P∋p
-          → ( p ⊆ q P∋p)   ∧ ( p ⊆ r P∋p)  
-          → ∀ ( s : HOD ) →  Power P ∋ s → ¬ (( q P∋p  ⊆ s  ) ∧ ( r P∋p  ⊆ s ))
+      q r : HOD
+      PP∋q : q ⊆ P 
+      PP∋r : r ⊆ P 
+      p⊆q :  p ⊆ q 
+      p⊆r :  p ⊆ r 
+      incompatible : ∀ ( s : HOD ) → s ⊆ P → (¬ ( q ⊆ s  )) ∨ (¬ ( r ⊆ s ))
 
 lemma725 : (P p : HOD ) (C : CountableModel P) 
-    →  * (ctl-M C) ∋ Power P
-    →  Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p {!!} C )))
-lemma725 = {!!}
+    →  (pp0 : Power P ∋ p )
+    →  * (ctl-M C) ∋ (Power P ∩  * (ctl-M C))                -- M is a Model of ZF
+    →  * (ctl-M C) ∋ ( (Power P ∩  * (ctl-M C))  ＼ filter ( genf ( P-GenericFilter P p pp0 C)) )      -- M ∋ G and M is a Model of ZF 
+    →  ((p : HOD) → (PP∋p : p  ⊆ P ) → Incompatible P p PP∋p )
+    → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p pp0 C )))
+lemma725 P p C PP∋p M∋PM M∋D I M∋G = D∩G≠∅ D∩G=∅ where
+    G = filter ( genf ( P-GenericFilter P p PP∋p C ))
+    M = * (ctl-M C)
+    D : HOD
+    D = Power P ＼ G
+    p⊆P : p ⊆ P
+    p⊆P =  ODC.power→⊆ O _ _ PP∋p
+    df : {x : HOD} → x ⊆ P → HOD
+    df {x} PP∋x with Incompatible.incompatible (I p p⊆P) x PP∋x
+    ... | case1 q = Incompatible.q (I p p⊆P) 
+    ... | case2 r = Incompatible.r (I p p⊆P) 
+    df-d : {x : HOD} → (lt : x ⊆ P) → D ∋ df lt
+    df-d = {!!}
+    df-p : {x : HOD} → (lt : x ⊆ P) → x ⊆ df lt
+    df-p = {!!}
+    D-Dense : Dense P
+    D-Dense = record {
+           dense = D
+       ;   d⊆P = record { incl = λ {x} lt → proj1 lt }
+       ;   dense-f = df
+       ;   dense-d = df-d
+       ;   dense-p = df-p
+     }
+    D∩G=∅ : ( D ∩ G ) =h= od∅ 
+    D∩G=∅ = {!!}
+    D∩G≠∅ : ¬ (( D ∩ G ) =h= od∅ )
+    D∩G≠∅ eq = generic (P-GenericFilter P p PP∋p C) D-Dense ( ==→o≡ eq )
 
 open import PFOD O
 
@@ -222,11 +249,11 @@
 -- ω→2 : HOD
 -- ω→2 = Power infinite
 
-lemma725-1 :   Incompatible HODω2
+lemma725-1 :  (p : HOD) → (PP∋p : p  ⊆ HODω2 ) → Incompatible HODω2 p PP∋p
 lemma725-1 = {!!}
 
 lemma726 :  (C : CountableModel HODω2) 
-    →  Union ( Replace HODω2 (λ p → filter ( genf ( P-GenericFilter HODω2 p {!!} C )))) =h= ω→2
+    →  Union ( Replace' (Power HODω2) (λ p lt → filter ( genf ( P-GenericFilter HODω2 p lt C )))) =h= ω→2 -- HODω2 ∋ p
 lemma726 = {!!}
 
 --
diff -r be685f338fdc -r b27d92694ed5 src/ordinal.agda
--- a/src/ordinal.agda	Sun Mar 13 19:22:12 2022 +0900
+++ b/src/ordinal.agda	Mon Mar 14 17:51:16 2022 +0900
@@ -200,26 +200,6 @@
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
       lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
---  record CountableOrdinal {n : Level} : Set (suc (suc n)) where
---     field
---         ctl→ : Nat → Ordinal {suc n}
---         ctl← : Ordinal → Nat
---         ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x
---         ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
---  
---  is-C-Ordinal : {n : Level} → CountableOrdinal {n}
---  is-C-Ordinal {n} = record {
---         ctl→ = {!!} 
---      ;  ctl← = λ x → TransFinite {n} (λ lx lt → Zero ) ctl01 x
---      ;  ctl-iso→ = {!!}
---      ;  ctl-iso← = {!!}
---    } where
---        ctl01 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → Nat) → Nat
---        ctl01 Zero (Φ Zero) prev = Zero 
---        ctl01 Zero (OSuc Zero x) prev = Suc ( prev (ordinal Zero x) (ordtrans <-osuc <-osuc )) 
---        ctl01 (Suc lx) (Φ (Suc lx)) prev = Suc ( prev (ordinal lx {!!}) {!!})
---        ctl01 (Suc lx) (OSuc (Suc lx) x) prev = Suc ( prev (ordinal (Suc lx) x) (ordtrans <-osuc <-osuc ))
-
 open import Ordinals 
 
 C-Ordinal : {n : Level} →  Ordinals {suc n} 
@@ -280,3 +260,9 @@
         caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
 
 
+-- H-Ordinal : {n : Level} → Ordinals {suc n} →  Ordinals {suc n}  →  Ordinals {suc n} 
+-- H-Ordinal {n} O1 O2 = record {
+--      Ordinal = Ordinals.Ordinal O1 ∧ Ordinals.Ordinal O2 
+--   }
+-- We may have an oridinal as proper subset  of an ordinal
+--   then the internal ordinal become a set in the outer ordinal