# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1569828855 -32400
# Node ID 9bf100ae50ac8b86059fb2de8b1f03c5cd9ff38b
# Parent  fee0fab14de032d304eb2c92185bd2372738c86c
filter

diff -r fee0fab14de0 -r 9bf100ae50ac filter.agda
--- a/filter.agda	Mon Sep 23 10:43:48 2019 +0900
+++ b/filter.agda	Mon Sep 30 16:34:15 2019 +0900
@@ -22,66 +22,26 @@
 open _∨_
 open Bool
 
-record Filter  ( P max : OD  )  : Set (suc n) where
-   field
-       _⊇_ : OD  → OD  → Set n
-       G : OD 
-       G∋1 : G ∋ max
-       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 :   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  ( P : Nat → Set n)  : Set (suc n) where
+record Filter  ( L : OD  ) : Set (suc n) where
    field
-       GN : Nat → Set n
-       GN∋1 : GN 0
-       GNmax : { p : Nat } → P p →  0 ≤ p 
-       GNless : { p q : Nat } → GN p → P q →  q ≤ p  → GN q
-       Gr : (  p q : Nat ) →  GN p → GN q  →  Nat
-       GNcompat : { p q : Nat }  → (gp : GN p) → (gq : GN q ) → (  Gr p q gp gq ≤  p ) ∨ (  Gr p q gp gq ≤ q )
+       F1 : { p q : OD  } → L ∋ p →  od→ord p o< od→ord q  → L ∋ q
+       F2 : { p q : OD  } → L ∋ p →  L ∋ q  → def L (minα (od→ord p ) (od→ord q ))
 
-record NatDense {n : Level} ( P : Nat → Set n)  : Set (suc n) where
-   field
-       Gmid : { p : Nat } → P p  → Nat
-       GDense : { D : Nat → Set n } → {x p : Nat } → (pp : P p ) → D (Gmid {p} pp) →  Gmid pp  ≤ p 
+open Filter
 
-open OD.OD
-
--- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
+proper-filter : {L : OD} → Filter L → Set n
+proper-filter {L} P = ¬ ( L ∋ od∅ )
 
-Pred :  ( Dom : OD  ) → OD 
-Pred  dom = record {
-      def = λ x → def dom x → {!!}
-  }
+prime-filter : {L : OD} → Filter L → {p q : OD } → Set n
+prime-filter {L} P {p} {q} =  def L ( maxα ( od→ord p ) (od→ord  q )) → ( L ∋ p ) ∨ ( L ∋ q )
 
-Hω2 :   OD 
-Hω2  = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) }
+ultra-filter :  {L : OD} → Filter L → {p : OD } → Set n 
+ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p ))
 
-Hω2Filter :     Filter  Hω2 od∅
-Hω2Filter  = record {
-       _⊇_ = _⊇_
-     ; G = {!!}
-     ; G∋1 = {!!}
-     ; Gmax = {!!}
-     ; Gless = {!!}
-     ; Gcompat = {!!}
-  } where
-       P = Hω2
-       _⊇_ : OD  → OD  → Set n
-       _⊇_ = {!!}
-       G : OD 
-       G = {!!}
-       G∋1 : G ∋ od∅
-       G∋1 = {!!}
-       Gmax : { p : OD  } → P ∋ p → p ⊇  od∅
-       Gmax = {!!}
-       Gless : { p q : OD  } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
-       Gless = {!!}
-       Gcompat : { p q : OD  } → G ∋ p → G ∋ q → ¬ (
-           ( r : OD ) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
-       Gcompat = {!!}
+-- H(ω,2) = Lower ( Lower ω ) = Def ( Def ω))
 
+postulate
+   dist-ord : {p q r : Ordinal } → minα p ( maxα q r ) ≡ maxα  ( minα p q ) ( minα p r )
+
+filter-lemma1 :  {L : OD} → (P : Filter L)  → {p q : OD } → ( (p : OD) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
+filter-lemma1 {L} P {p} {q} u lt = {!!}