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 = {!!}