--- a/filter.agda	Sun Jul 19 19:57:59 2020 +0900
+++ b/filter.agda	Mon Jul 20 12:17:43 2020 +0900
@@ -53,6 +53,9 @@
 trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
 
+refl-⊆ : {A : HOD} → A ⊆ A
+refl-⊆ {A} = record { incl = λ x → x }
+
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
    t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
@@ -180,28 +183,44 @@
 record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where
    field
      gn  : Nat
-     f<n :  p f⊆ (f ↑ gn)
+     f<n :  (f ↑ gn) f⊆ p
 
 open Gf
 
-record F-Filter (L : Set (suc n)) (PL : (L → Set (suc n)) → Set n) ( _⊆_ : L  → L → Set (suc n))  (_∩_ : L → L → L ) : Set (suc (suc n)) where
+record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
    field
-       filter : L → Set (suc n)
+       filter : L → Set n
        f⊆P :  PL filter 
-       filter1 : { p q : L } → filter p →  p ⊆ q  → filter q
+       filter1 : { p q : L } → PL (λ x → q ⊆ x )  → filter p →  p ⊆ q  → filter q
        filter2 : { p q : L } → filter p →  filter q  → filter (p ∩ q)
 
-GF : (Nat → Two ) → F-Filter PFunc (λ x → One) _f⊆_ _f∩_
+Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
+Filter-is-F {L} f = record {
+       filter = λ x → Lift (suc n) ((filter f) ∋ x)
+     ; f⊆P = λ x f∋x →  power→⊆ _ _ (incl ( f⊆PL f  ) (lower f∋x ))
+     ; filter1 = λ {p} {q} q⊆L f∋p  p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q)
+     ; filter2 = λ {p} {q} f∋p f∋q  → lift ( filter2 f (lower f∋p) (lower f∋q)) 
+    }
+
+min  = Data.Nat._⊓_
+-- m≤m⊔n  = Data.Nat._⊔_
+open import Data.Nat.Properties
+
+GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_
 GF f = record {  
        filter = λ p → Gf f p
-     ; f⊆P = OneObj
-     ; filter1 = λ {p} {q} fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
-     ; filter2 = λ {p} {q} fp fq  → record { gn = gn fp ; f<n = f2 fp fq }
+     ; f⊆P = lift OneObj
+     ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
+     ; filter2 = λ {p} {q} fp fq  → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq }
  } where
-     f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → q f⊆ (f ↑ gn fp)
-     f1 {p} {q} fp p⊆q = record { extend = λ x fq → {!!}  ; feq = λ x fr → {!!} } where
-     f2 : {p q : PFunc } → (fp : Gf f p ) → (fq : Gf f q ) → (p f∩ q) f⊆ (f ↑ gn fp)
-     f2 {p} {q} fp fq  = record { extend = λ  x y → extend (f<n fp) x (proj1 y) ; feq = λ x fr → {!!} } where
+     f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q
+     f1 {p} {q} fp p⊆q = record { extend = λ x x<g → extend p⊆q x (extend (f<n fp ) x x<g) ; feq = λ x fr → {!!} } where
+     f2 : {p q : PFunc } → (fp : Gf f p ) → (fq : Gf f q ) → (f ↑ (min (gn fp) (gn fq)))  f⊆ (p f∩ q)
+     f2 {p} {q} fp fq  = record { extend = λ  x x<g → record {
+           proj1 = extend (f<n fp ) x (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))
+         ; proj2 = record {proj1 = extend (f<n fq ) x (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))
+         ;                 proj2 = {!!} }}  ;
+        feq = λ x fr → {!!} } where
 
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y))