--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/filter.agda	Fri Jul 26 21:08:06 2019 +0900
@@ -0,0 +1,65 @@
+open import Level
+module filter where
+
+open import zf
+open import ordinal
+open import OD
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+open import Relation.Binary
+open import Relation.Binary.Core
+open import  Relation.Binary.PropositionalEquality
+
+record Filter {n : Level} ( P max : OD {suc n} )  : Set (suc (suc n)) where
+   field
+       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
+       G : OD {suc n}
+       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 )))
+
+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 ))
+
+open OD.OD
+
+-- 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
+  }
+
+Hω2 : {n : Level} →  OD {suc n}
+Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) }
+
+_⊆_ : {n : Level} → ( A B : OD {suc n}  ) → ∀{ x : OD {suc n} } →  Set (suc n)
+_⊆_ A B {x} = A ∋ x →  B ∋ x
+
+Hω2Filter :   {n : Level} → Filter {n} Hω2 od∅
+Hω2Filter {n} = record {
+       _⊇_ = {!!}
+     ; G = {!!}
+     ; G∋1 = {!!}
+     ; Gmax = {!!}
+     ; Gless = {!!}
+     ; Gcompat = {!!}
+  } where
+       P = Hω2
+       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
+       _⊇_ = {!!}
+       G : OD {suc n}
+       G = {!!}
+       G∋1 : G ∋ od∅
+       G∋1 = {!!}
+       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  od∅
+       Gmax = {!!}
+       Gless : { p q : OD {suc n} } → 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 = {!!}
+