--- a/filter.agda	Sun Jul 28 14:50:56 2019 +0900
+++ b/filter.agda	Mon Jul 29 08:41:16 2019 +0900
@@ -1,9 +1,9 @@
 open import Level
-module filter where
-
+open import OD
 open import zf
 open import ordinal
-open import OD
+module filter ( n : Level )  where
+
 open import Relation.Nullary
 open import Relation.Binary
 open import Data.Empty
@@ -12,6 +12,8 @@
 open import  Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 
+od = OD→ZF {n}
+
 
 record Filter {n : Level} ( P max : OD {suc n} )  : Set (suc (suc n)) where
    field