--- a/filter.agda	Wed Jul 22 00:20:33 2020 +0900
+++ b/filter.agda	Wed Jul 22 08:08:04 2020 +0900
@@ -371,20 +371,6 @@
      lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y 
      lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y 
 
-lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t))
-lemma12 s t eq = eq
-lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t))
-lemma13 s t eq = eq
-lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t))
-lemma14 s t eq = eq
-
-record Finite3 (p : List Three ) : Set  where
-   field
-     3-max :  Nat 
-     3-func :  Nat → Two
-     3-p⊆f :  p 3⊆ (3-func 3↑ 3-max)
-     3-f⊆p :  (3-func 3↑ 3-max) 3⊆ p 
-
 Finite3b : (p : List Three ) → Bool 
 Finite3b [] = true
 Finite3b (j0 ∷ f) = Finite3b f
@@ -564,6 +550,22 @@
     ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
     ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
 
+3→Hω2 : List Three → HOD
+3→Hω2 t = list→hod t 0 where
+   list→hod : List Three → Nat → HOD
+   list→hod [] _ = od∅
+   list→hod (j0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) 
+   list→hod (j1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) 
+   list→hod (j2 ∷ t) i = list→hod t (Suc i ) 
+
+Hω2→3 : (x :  HOD) → HODω2 ∋ x → List Three 
+Hω2→3 x = lemma where
+   lemma : { y : Ordinal } →  Hω2r y → List Three
+   lemma record { count = 0 ; hω2 = hφ } = []
+   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = j0 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = j1 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (he hω3) } = j2 ∷ lemma record { count = i ; hω2 =  hω3 }
+
 ω→2 : HOD
 ω→2 = Replace (Power infinite) (λ p  → Replace infinite (λ x → < x , repl p x > )) where
   repl : HOD → HOD → HOD
@@ -571,17 +573,28 @@
   ... | yes _  = nat→ω 1
   ... | no _  = nat→ω 0
 
-record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where
-   -- field
-      -- n : HOD
-      -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n
-  
--- Gf : {f : HOD} → ω→2 ∋ f  → HOD
--- Gf {f} lt = Select HODω2 (λ x H∋x → {!!}   )
+ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
+ω→2f x = {!!}
+
+↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
+↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))
+
+record Gfo (x : Ordinal) : Set n where
+  field
+     gfunc : Ordinal
+     gmax : Ordinal
+     gcond : (odef ω→2  gfunc) ∧ (odef infinite gmax)
+     gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) )  ⊆ ord→od x 
+     pcond : odef HODω2 x
+
+open Gfo
+
+HODGf : HOD
+HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} }
 
 G : (Nat → Two) → Filter HODω2
 G f = record {
-       filter = {!!}
+       filter = HODGf
      ; f⊆PL = {!!}
      ; filter1 = {!!}
      ; filter2 = {!!}