# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1596878054 -32400
# Node ID 9b0630f03c4b85fef5ac0d261223492b19cc52bb
# Parent  47aacf417930c61e1b79ef736d370aaec315aa16
...

diff -r 47aacf417930 -r 9b0630f03c4b OD.agda
--- a/OD.agda	Thu Aug 06 11:50:35 2020 +0900
+++ b/OD.agda	Sat Aug 08 18:14:14 2020 +0900
@@ -199,6 +199,13 @@
 ord-od∅ : & (od∅ ) ≡ o∅ 
 ord-od∅  = sym ( subst (λ k → k ≡  & (od∅ ) ) &iso (cong ( λ k → & k ) o∅≡od∅ ) )
 
+≡o∅→=od∅  : {x : HOD} → & x ≡ o∅ → od x == od od∅
+≡o∅→=od∅ {x} eq = record { eq→ = λ {y} lt → ⊥-elim ( ¬x<0 {y} (subst₂ (λ j k → j o< k ) &iso eq ( c<→o< {* y} {x} (d→∋ x lt))))
+    ; eq← = λ {y} lt → ⊥-elim ( ¬x<0 lt )}  
+
+=od∅→≡o∅  : {x : HOD} → od x == od od∅ → & x ≡ o∅ 
+=od∅→≡o∅ {x} eq = trans (cong (λ k → & k ) (==→o≡ {x} {od∅} eq)) ord-od∅
+
 ∅0 : record { def = λ x →  Lift n ⊥ } == od od∅  
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} lt = lift (¬x<0 lt)
diff -r 47aacf417930 -r 9b0630f03c4b cardinal.agda
--- a/cardinal.agda	Thu Aug 06 11:50:35 2020 +0900
+++ b/cardinal.agda	Sat Aug 08 18:14:14 2020 +0900
@@ -49,25 +49,6 @@
     ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) } 
        ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
 
--- Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
---     → def Func (&  (Replace A (λ x → < x , f x > )))
--- Func∋f = {!!}
-
--- FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
---     → odef (FuncP A B) (&  (Replace A (λ x → < x , f x > )))
--- FuncP∋f = {!!}
-
--- Func→f : {A B f x : HOD} → def Func (& f)  → (x : HOD ) → A ∋ x  → ( HOD ∧ ((y : HOD ) → B ∋ y ))
--- Func→f = {!!}
--- Func₁ : {A B f : HOD} → def Func (& f) → {!!}  
--- Func₁ = {!!}
--- Cod : {A B f : HOD} → def Func (& f) → {!!}
--- Cod = {!!}
--- 1-1 : {A B f : HOD} → def Func (& f) → {!!}
--- 1-1 = {!!}
--- onto : {A B f : HOD} → def Func (& f) → {!!}
--- onto  = {!!}
-
 record Injection (A B : Ordinal ) : Set n where
    field
        i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
@@ -101,6 +82,12 @@
        ciso : Bijection a card
        cmax : (x : Ordinal) → card o< x → ¬ Bijection a x
 
+Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s →   s c< Ord t 
+Cardinal∈ = ?
+
+Cardinal⊆ : { s t : HOD } → s ⊆ t →  ( s c< t ) ∨ ( s =c= t )
+Cardinal⊆ = {!!}
+
 Cantor1 : { u : HOD } → u c< Power u
 Cantor1 = {!!}
 
diff -r 47aacf417930 -r 9b0630f03c4b generic-filter.agda
--- a/generic-filter.agda	Thu Aug 06 11:50:35 2020 +0900
+++ b/generic-filter.agda	Sat Aug 08 18:14:14 2020 +0900
@@ -185,16 +185,16 @@
 --
 PGHOD :  (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
 PGHOD i C P p = record { od = record { def = λ x  →
-       odef P x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
-   ; odmax = odmax P  ; <odmax = λ {y} lt → <odmax P (proj1 lt) }  
+       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
+   ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }  
 
 ---
 --   p(n+1) = if PGHOD n qn otherwise p(n)
 --
 next-p :  (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal
-next-p C P i p with ODC.decp O ( PGHOD i C P p =h= od∅ )
+next-p C P i p with is-o∅  ( & (PGHOD i C P p))  
 next-p C P i p | yes y = p
-next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) not)
+next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
 
 ---
 --  ascendant search on p(n)
@@ -210,7 +210,7 @@
    field
        gr : Nat
        pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y
-       px∈ω  : odef (Power P) x
+       x∈PP  : odef (Power P) x
 
 open PDN
 
@@ -219,7 +219,7 @@
 --
 PDHOD :  (C : CountableOrdinal) → (P : HOD ) → HOD
 PDHOD C P = record { od = record { def = λ x →  PDN C P x }
-    ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.px∈ω lt)  } where
+    ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt)  } where
 
 open PDN
 
@@ -230,17 +230,18 @@
 --  p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q  (axiom of choice)
 ---             else p n
 
+P∅ : {P : HOD} → odef (Power P) o∅
+P∅ {P} =  subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅  o∅≡od∅) where
+    lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
+    lemma x eq = power← P od∅  (λ {x} lt → ⊥-elim (¬x<0 lt ))
+x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
+x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
+
 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
 P-GenericFilter C P = record {
       genf = record { filter = PDHOD C P ; f⊆PL =  f⊆PL ; filter1 = {!!} ; filter2 = {!!} }
     ; generic = λ D → {!!}
    } where
-        P∅ : {P : HOD} → odef (Power P) o∅
-        P∅ {P} =  subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅  o∅≡od∅) where
-            lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
-            lemma x eq = power← P od∅  (λ {x} lt → ⊥-elim (¬x<0 lt ))
-        x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
-        x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
         find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y 
         find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso
             ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P)  Px)) (x<y→∋ Py))
@@ -274,7 +275,8 @@
 --
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --
+--   W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) |  { i ∈ Nat → p i ≠ i1 } is finite }
+--
 
 
 
-