# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1596064556 -32400
# Node ID b00d58b3dc579ee756d0957fef6c7f48e5c9a563
# Parent  38eded55c72d8bdfd364dca37d049061e254dcaa
generic filter on going

diff -r 38eded55c72d -r b00d58b3dc57 generic-filter.agda
--- a/generic-filter.agda	Thu Jul 30 00:29:50 2020 +0900
+++ b/generic-filter.agda	Thu Jul 30 08:15:56 2020 +0900
@@ -207,33 +207,39 @@
 open PDN
 
 ---
--- G as an HOD
+-- G as a HOD
 --
 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
 
---
---  p 0 ≡ ∅
---  p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q 
----             else p n
-
 open PDN
 
 ----
---  Generic Filter on Power P for HOD's Ordinal
+--  Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set )
 --
+--  p 0 ≡ ∅
+--  p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q  (axiom of choice)
+---             else p n
+
 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
-        find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal)  → odef (ord→od (find-p C P i x)) y → odef P y 
-        find-p-⊆P C P Zero x y Py = {!!} 
-        find-p-⊆P C P (Suc i) x y Py = {!!} -- find-p-⊆P C P i x {!!}
+        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 ) → ord→od x ≡ od∅ → odef (Power P) (od→ord od∅)
+            lemma x eq = power← P od∅  (λ {x} lt → ⊥-elim (¬x<0 lt ))
+        x<y→∋ : {x y : Ordinal} → odef (ord→od x) y → ord→od x ∋ ord→od y
+        x<y→∋ {x} {y} lt = subst (λ k → odef (ord→od x) k ) (sym diso) lt
+        find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (ord→od (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 ) diso
+            ( incl (ODC.power→⊆ O P (ord→od x) (d→∋ (Power P)  Px)) (x<y→∋ Py))
+        find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p C P i x)  y {!!} {!!}
         f⊆PL :  PDHOD C P ⊆ Power P
         f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
-             find-p-⊆P C P (gr lt) o∅ (od→ord y) (pn<gr lt (od→ord y) (subst (λ k → odef k (od→ord y)) (sym oiso) y<x))) }
+             find-p-⊆P C P (gr lt) o∅ (od→ord y) P∅ (pn<gr lt (od→ord y) (subst (λ k → odef k (od→ord y)) (sym oiso) y<x))) }
 
 
 open GenericFilter