--- a/filter.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/filter.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -1,8 +1,10 @@
 open import Level
-open import OD
+open import Ordinals
+module filter {n : Level } (O : Ordinals {n})   where
+
 open import zf
-open import ordinal
-module filter ( n : Level )  where
+open import logic
+import OD 
 
 open import Relation.Nullary
 open import Relation.Binary
@@ -12,23 +14,28 @@
 open import  Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 
-od = OD→ZF {n}
-
+open inOrdinal O
+open OD O
+open OD.OD
 
-record Filter {n : Level} ( P max : OD {suc n} )  : Set (suc (suc n)) where
+open _∧_
+open _∨_
+open Bool
+
+record Filter  ( P max : OD  )  : Set (suc n) where
    field
-       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
-       G : OD {suc n}
+       _⊇_ : OD  → OD  → Set n
+       G : OD 
        G∋1 : G ∋ max
-       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  max 
-       Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
-       Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
-           ( r : OD {suc n}) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
+       Gmax : { p : OD  } → P ∋ p → p ⊇  max 
+       Gless : { p q : OD  } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gcompat : { p q : OD  } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD ) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
 
-dense :  {n : Level} → Set (suc (suc n))
-dense {n} = { D P p : OD {suc n} } → ({x : OD {suc n}} → P ∋ p → ¬ ( ( q : OD {suc n}) → D ∋ q → od→ord p o< od→ord q ))
+dense :   Set (suc n)
+dense = { D P p : OD  } → ({x : OD } → P ∋ p → ¬ ( ( q : OD ) → D ∋ q → od→ord p o< od→ord q ))
 
-record NatFilter {n : Level} ( P : Nat → Set n)  : Set (suc n) where
+record NatFilter  ( P : Nat → Set n)  : Set (suc n) where
    field
        GN : Nat → Set n
        GN∋1 : GN 0
@@ -46,16 +53,16 @@
 
 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
 
-Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n}
-Pred {n} dom = record {
-      def = λ x → def dom x → Set n
+Pred :  ( Dom : OD  ) → OD 
+Pred  dom = record {
+      def = λ x → def dom x → {!!}
   }
 
-Hω2 : {n : Level} →  OD {suc n}
-Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) }
+Hω2 :   OD 
+Hω2  = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) }
 
-Hω2Filter :   {n : Level} → Filter {n} Hω2 od∅
-Hω2Filter {n} = record {
+Hω2Filter :     Filter  Hω2 od∅
+Hω2Filter  = record {
        _⊇_ = _⊇_
      ; G = {!!}
      ; G∋1 = {!!}
@@ -64,17 +71,17 @@
      ; Gcompat = {!!}
   } where
        P = Hω2
-       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
+       _⊇_ : OD  → OD  → Set n
        _⊇_ = {!!}
-       G : OD {suc n}
+       G : OD 
        G = {!!}
        G∋1 : G ∋ od∅
        G∋1 = {!!}
-       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  od∅
+       Gmax : { p : OD  } → P ∋ p → p ⊇  od∅
        Gmax = {!!}
-       Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gless : { p q : OD  } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
        Gless = {!!}
-       Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
-           ( r : OD {suc n}) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
+       Gcompat : { p q : OD  } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD ) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
        Gcompat = {!!}