--- a/filter.agda	Fri Jul 17 18:57:40 2020 +0900
+++ b/filter.agda	Sat Jul 18 10:36:32 2020 +0900
@@ -6,14 +6,14 @@
 open import logic
 import OD 
 
-open import Relation.Nullary
-open import Relation.Binary
-open import Data.Empty
+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
+open import Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-import BAlgbra
+import BAlgbra 
 
 open BAlgbra O
 
@@ -131,13 +131,6 @@
        dense-d :  { p : HOD} → P ∋ p  → dense ∋ dense-f p  
        dense-p :  { p : HOD} → P ∋ p  →  p ⊆ (dense-f p) 
 
---    the set of finite partial functions from ω to 2
---
---   ph2 : Nat → Set → 2
---   ph2 : Nat → Maybe 2
---
--- Hω2 : Filter (Power (Power infinite))
-
 record Ideal  ( L : HOD  ) : Set (suc n) where
    field
        ideal : HOD   
@@ -153,3 +146,45 @@
 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
 prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
 
+--    the set of finite partial functions from ω to 2
+--
+--   ph2 : Nat → Set → 2
+--   ph2 : Nat → Maybe 2
+--
+-- Hω2 : Filter (Power (Power infinite))
+
+import OPair
+open OPair O
+
+ODSuc : (y : HOD) → infinite ∋ y → HOD
+ODSuc y lt = Union (y , (y , y)) 
+
+nat→ω : Nat → HOD
+nat→ω Zero = od∅
+nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
+
+data Hω2 : ( x : Ordinal  ) → Set n where
+  hφ :  Hω2 o∅
+  h0 : {x : Ordinal  } → Hω2 x  →
+    Hω2 (od→ord < nat→ω 0 , ord→od x >)
+  h1 : {x : Ordinal  } → Hω2 x  →
+    Hω2 (od→ord < nat→ω 1 , ord→od x >)
+  h2 : {x : Ordinal  } → Hω2 x  →
+    Hω2 (od→ord < nat→ω 2 , ord→od x >)
+
+HODω2 :  HOD
+HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = {!!} ; <odmax = {!!} }
+
+-- the set of finite partial functions from ω to 2
+
+data Two : Set n where
+   i0 : Two
+   i1 : Two
+
+Hω2f : Set (suc n)
+Hω2f = (Nat → Set n) → Two
+
+Hω2f→Hω2 : Hω2f  → HOD
+Hω2f→Hω2 p = record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
+
+